]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f740ba9) | patch
Management of automatic insertion of aliases and "goal" commands reimplemented
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 08:46:26 +0000 (08:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 08:46:26 +0000 (08:46 +0000)
commit2c2474e19e7cd5d271328823a13d2e75a3557da2
tree05c4786d5de58ab38a5e17b55c0fb6001dad9abftree | snapshot
parentf740ba9bd597dad3d2edede01433fd31cbb79bb7commit | diff
Management of automatic insertion of aliases and "goal" commands reimplemented
almost from scratch. The new commands inserted are now distinct entities in
the history. As a consequence going up in the script is now a step by step
operation and going up and going down are invertible operations, as they
should be.
helm/matita/matita.txt diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.