]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af73dd5) | patch
1. MatitaGuiTypes.gui interface streamlined
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Dec 2010 15:06:10 +0000 (15:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Dec 2010 15:06:10 +0000 (15:06 +0000)
commiteebe90eef0aa7997fc6cfc926b7bbf1899b5080d
tree0e5e8bc4fda07af0cdb7cbf3eb20974023f372c1tree | snapshot
parentaf73dd5916c5505e8285766f0e3a48a8693943efcommit | diff
1. MatitaGuiTypes.gui interface streamlined
2. added new menu item to close a script
3. restored graying of "Save" menu item when the script is unnamed
matita/matita/matita.glade diff | blob | history
matita/matita/matitaGui.ml diff | blob | history
matita/matita/matitaGuiTypes.mli diff | blob | history
matita/matita/matitaScript.ml diff | blob | history
matita/matita/matitaScript.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.