]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8178b14) | 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)
commit3347eb56c6951e39e7d7b375198ab819dffcdf1b
treeeb765b64ca81da4fce525bf9b137bd3c0776f568tree | snapshot
parent8178b146713be49b5d21744d2cc68d3d4af726a3commit | 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.
components/grafite_parser/grafiteDisambiguator.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.