]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5aa4da5) | patch
since there is no more tab, the modification of the current file is in the window...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Nov 2007 21:14:49 +0000 (21:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Nov 2007 21:14:49 +0000 (21:14 +0000)
commit1f252a3fe87fa261028d026235be17ef02596c97
treef56d18e0981aecb492c1f2d412b41647b77f851ftree | snapshot
parent5aa4da5846c72942f3d204f71ecfba8d6cc7911bcommit | diff
since there is no more tab, the modification of the current file is in the window title
matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.