]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 98016b0) | patch
fixed a problem when newScript was called
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 7 Jul 2005 08:41:05 +0000 (08:41 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 7 Jul 2005 08:41:05 +0000 (08:41 +0000)
commit10df455f8e84b4b1f793e26d432dc19ba4ee93a0
tree3013b92ea540763e77faa063cacfe201c2121fb7tree | snapshot
parent98016b0996c55891b7fbf85d0ead98235441b14fcommit | diff
fixed a problem when newScript was called
(the filename was not resetted properly)
helm/matita/matitaGui.ml diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.