]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 53182a6) | patch
1. Warnings are now printed in orange (yellow was unvisible on a white
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jul 2005 15:33:18 +0000 (15:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jul 2005 15:33:18 +0000 (15:33 +0000)
commit6a78ec39e3f2ddceb9d0836e6c2a494aa0f2e421
treed6d0b1f5c7a1e9aebc68b0eba5b3037b0b61c2fftree | snapshot
parent53182a673b2f3673fe9e878f373a8bafe6f65f75commit | diff
1. Warnings are now printed in orange (yellow was unvisible on a white
   background!)
2. the "Bad name" error is now a "Bad name" warning
helm/matita/matitaEngine.ml diff | blob | history
helm/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.