]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fe24653) | patch
Removed rebuilding of urls_of_uris.db on update user request.
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Feb 2001 21:29:36 +0000 (21:29 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Feb 2001 21:29:36 +0000 (21:29 +0000)
commitc1dfb763206c3e548b26d1e5f2128c6938a5df14
treeef73f74e8f281533546afa1ad2467bfadf39bf45tree | snapshot
parentfe24653b699d2fdb49834653dd8480438c9dc545commit | diff
Removed rebuilding of urls_of_uris.db on update user request.
This feature now is handled by http_getter.
Also modified file 'http_getter.pl.in' from module 'http_getter'.
helm/interface/getter.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.