]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 586fd6f) | 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)
commit3da15a10eadcba9a0d9cef36f2e66e6c9b076d32
tree57238a23c3241627c5107beb80df3f8f74f464c3tree | snapshot
parent586fd6f56b845612e60a80f17f8070d13be52660commit | 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
matita/matitaInit.ml diff | blob | history
matita/matitamake.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.