]> matita.cs.unibo.it Git - helm.git/commit
added "are you sure you want to quit with usaved script?"
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 28 Jun 2005 10:58:10 +0000 (10:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 28 Jun 2005 10:58:10 +0000 (10:58 +0000)
commit030d34e0dc025b94d7f0459eff0a84e2ac108b73
tree11e3a1612bce0fe58792d0f534228c96faf3122b
parent6a9d597352e104434a1a7f371fdd1bbdac5e50a3
added "are you sure you want to quit with usaved script?"
helm/matita/matitaGtkMisc.ml
helm/matita/matitaGtkMisc.mli
helm/matita/matitaGui.ml
helm/matita/matitaMathView.ml