]> matita.cs.unibo.it Git - helm.git/commit
compilation of needed modules now outputs to the log window
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 Jul 2005 13:03:03 +0000 (13:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 Jul 2005 13:03:03 +0000 (13:03 +0000)
commitecd0ab19b82f611974bd76f3c740c842f566009d
tree1f6e0a9abe072bdcbb9f171c6f320a3e5021255e
parent6b5e1d495c61f459738187e8d71efadb162abdbe
compilation of needed modules now outputs to the log window
helm/matita/.depend
helm/matita/Makefile.in
helm/matita/matitaGui.ml
helm/matita/matitaScript.ml
helm/matita/matitamakeLib.ml
helm/matita/matitamakeLib.mli