]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a092d97) | patch
added \n to "file saved" message
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)
commit088377896f207fac6f53c4e4d43df1cb3b7a9589
treef510e7a6f8dc1b8ad4f084576d41a88d1526324etree | snapshot
parenta092d97f720a9241d77d987a72cdb810c1d88212commit | diff
added \n to "file saved" message
helm/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.