]> matita.cs.unibo.it Git - helm.git/commit
MatitacleanLib.remove_baseuris will remove empty directories.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Sep 2005 12:32:26 +0000 (12:32 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Sep 2005 12:32:26 +0000 (12:32 +0000)
commitd7c24dbca4f5e2baef606669db70cc640c02d38d
treea8acbf2bffe48834b0a5d15826ca24df44b146f6
parentc3b6e22034e3029195031d31c94983c381ae659b
MatitacleanLib.remove_baseuris will remove empty directories.
helm/matita/matita.txt
helm/matita/matitaMisc.ml
helm/matita/matitaMisc.mli
helm/matita/matitaSync.ml
helm/matita/matitacleanLib.ml