]> matita.cs.unibo.it Git - helm.git/commit
better handling of backgroud compiler process
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 20 Jul 2005 13:51:30 +0000 (13:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 20 Jul 2005 13:51:30 +0000 (13:51 +0000)
commit7c0db1e564918026d56e81163b4f1e4aee649055
tree11248911cdcf3ccf6fa2dba1791d5c64d653d21e
parent92500502aa145675b685cf9d81803c0bdcb2d6b8
better handling of backgroud compiler process
helm/matita/matitaExcPp.ml
helm/matita/matitaGui.ml
helm/matita/matitamakeLib.ml