]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1e6052) | patch
minimal changes:
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Mar 2003 15:07:17 +0000 (15:07 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Mar 2003 15:07:17 +0000 (15:07 +0000)
commitdfa2ac7a7c291b58e445d005438ea7f535d466bf
treeee9ebdeb24399fcbfb78c4747472e3c9ca37a51dtree | snapshot
parenta1e60521d58ed2a10e66539ee3bbc3392ddf41b2commit | diff
minimal changes:
- added a TODO comment
- factorized some code
- removed old useless debugging prints
helm/searchEngine/searchEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.