why3doc: if no output dir given, do not substitute / by . in filename, so as to keep the full path unchanged
why3doc: if no output dir given, do not substitute / by . in filename,
so as to keep the full path unchanged

ssaavedra/why3,ssaavedra/why3,ssaavedra/why3