]> matita.cs.unibo.it Git - helm.git/commit
better handling of script names
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 30 Jun 2005 09:32:45 +0000 (09:32 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 30 Jun 2005 09:32:45 +0000 (09:32 +0000)
commitab0d1d5a50ad2e01bcf2e5e4a6ded8322a9da4b9
tree1d9116099397a433e06eecd4aa5a4d243fa687e8
parentced6c94c59ba147abbee642dcd3e816ee2e1c1eb
better handling of script names
helm/matita/matitaScript.ml
helm/matita/matitaScript.mli