]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1e2ad35) | patch
1. select_all added to the Edit menu; no shortcut for it (since the standard
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Jul 2005 13:49:50 +0000 (13:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Jul 2005 13:49:50 +0000 (13:49 +0000)
commit651f406cbaee8309ea80f1205696a355ff31cd2f
tree499f03f9a4e2682a41f5dc45ffa22b15dc48da5btree | snapshot
parent1e2ad3511cad89d422ccd0bc46939522c846e56dcommit | diff
1. select_all added to the Edit menu; no shortcut for it (since the standard
   one (Ctr+A) hides the Emacs-like binding "go to beginning of line")
2. added a few standard but missing shortcuts (Ctr-N for a new document,
   Shift+Ctr+S for save as)
helm/matita/matita.glade diff | blob | history
helm/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.