]> matita.cs.unibo.it Git - helm.git/commit
matita now asks to save .moo if possible or cleans the dust the
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 6 Jul 2005 10:02:58 +0000 (10:02 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 6 Jul 2005 10:02:58 +0000 (10:02 +0000)
commit646ade789430669f4a6be3ecbf47d89fe865f132
treea7005c0f48057d4a7962fcb5bf02673f14169ad1
parent1b3aa3daa64f8b68aa08ff1c5458ba828398f897
matita now asks to save .moo if possible or cleans the dust the
execution has produced
helm/matita/Makefile.in
helm/matita/matitaGui.ml
helm/matita/matitaScript.ml
helm/matita/matitaScript.mli
helm/matita/matitacLib.mli
helm/matita/matitacleanLib.ml