-
MARCHE Claude authored
no empty dir will be created with a name having an extension, eg why3 ide file.mlw will now signal an error if file.mlw does not exist side effect: Open_Session request is disabled, will see if we want it later
7dda1c7d
Prochaines maintenances programmées: lundi 06/05, lundi 03/06, lundi 01/07
Pour plus d'informations: https://doc-si.inria.fr/display/SU/Gitlab
no empty dir will be created with a name having an extension, eg why3 ide file.mlw will now signal an error if file.mlw does not exist side effect: Open_Session request is disabled, will see if we want it later