]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e1dee09) | patch
Aliases are now wrote down even during the first pass.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Sep 2006 13:40:01 +0000 (13:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Sep 2006 13:40:01 +0000 (13:40 +0000)
commit7c24781a5668273116bb64e93e56f4ab1ab3fede
tree3cc4cf7ff1a2c6652b9d3024758302d9bf27913btree | snapshot
parente1dee095df33ef99ad011bc30eeb256f31ffdf10commit | diff
Aliases are now wrote down even during the first pass.
The only case they are not written down is that of multiple passes.
This makes the scripts more robusts and faster.
We still need (more and more) one shot aliases.
helm/software/components/grafite_parser/grafiteDisambiguator.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.