]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2817260) | patch
Bug fixed: matitaclean and matitadep now ignores every parsing errors and
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 19 Jul 2005 09:57:55 +0000 (09:57 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 19 Jul 2005 09:57:55 +0000 (09:57 +0000)
commitb8193e0717e01edfcf826a6edce0866496537e8a
tree616def061f461fe3198a5f609623409121f31653tree | snapshot
parent2817260358878e72fa359c6d2431b4c7c358a841commit | diff
Bug fixed: matitaclean and matitadep now ignores every parsing errors and
simply continues. Before it used to avoid cleaning things and --- much worst ---
generating an empty .depend.
helm/matita/matitacleanLib.ml diff | blob | history
helm/matita/matitadep.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.