]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 58cda4a) | patch
- uniformed command line handling of matitamake with that of other matita tools
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 6 Feb 2006 17:19:28 +0000 (17:19 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 6 Feb 2006 17:19:28 +0000 (17:19 +0000)
commit76566c28a29c9f80bea13fb72c57d6a881fb3544
treea0e47cfd0666f16ec687708d838e241a59bc397ctree | snapshot
parent58cda4ac5c0fcdba36993496e607fe326757a896commit | diff
- uniformed command line handling of matitamake with that of other matita tools
- changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1
  unit
- added "-v" flag: it increase the "matita.verbosity" value by 1
- "matita.quiet" is no longer in use
helm/software/matita/matitaInit.ml diff | blob | history
helm/software/matita/matitamake.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.