]> matita.cs.unibo.it Git - helm.git/commit
matita now includes compiling. if the file is not compiled it compiles it,
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 6 Jan 2008 22:35:53 +0000 (22:35 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 6 Jan 2008 22:35:53 +0000 (22:35 +0000)
commitb36918dbc0e6d0c70c92551e34bdc65cbfddddec
treee65978fa1a9081c3c3041224b03522c889889da7
parent54e4c7dc896732bafcd907b0380d59efa0a181b7
matita now includes compiling. if the file is not compiled it compiles it,
but if it is compiled it does not check that it may need to be rebuilt
components/library/librarian.mli
matita/matitaGui.ml
matita/matitaScript.ml
matita/matitaScript.mli