]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f405e16) | patch
bugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Oct 2004 12:44:13 +0000 (12:44 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Oct 2004 12:44:13 +0000 (12:44 +0000)
commit17a935085d171c7ba4d9894931bfe6c74dc93528
tree0db21b2188dd67eb2f1710ca435023bef86c6ac4tree | snapshot
parentf405e161079f553f31138699b583f9000e48e401commit | diff
bugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
implementation: filter out variables)
helm/searchEngine/searchEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.