matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Stefano Zacchiroli <zack@upsilon.cc>
	Tue, 5 Jul 2005 08:09:24 +0000 (08:09 +0000)
committer	Stefano Zacchiroli <zack@upsilon.cc>
	Tue, 5 Jul 2005 08:09:24 +0000 (08:09 +0000)
commit	a3fb06e72407e3590fa60a74ac5fec01e6bfe1f9
tree	855820521c1f1725d9d83b76276bb1f969040e5e	tree \| snapshot
parent	a83e0e4b2cf4d0cd378b5f2f451aa857507e0a01	commit \| diff

new getter implementation: no more DBM maps

26 files changed:

helm/ocaml/getter/.depend		diff \| blob \| history
helm/ocaml/getter/.ocamlinit	[new file with mode: 0644]	blob
helm/ocaml/getter/Makefile		diff \| blob \| history
helm/ocaml/getter/http_getter.ml		diff \| blob \| history
helm/ocaml/getter/http_getter.mli		diff \| blob \| history
helm/ocaml/getter/http_getter_cache.ml	[deleted file]	blob \| history
helm/ocaml/getter/http_getter_cache.mli	[deleted file]	blob \| history
helm/ocaml/getter/http_getter_common.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_common.mli		diff \| blob \| history
helm/ocaml/getter/http_getter_const.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_env.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_env.mli		diff \| blob \| history
helm/ocaml/getter/http_getter_md5.ml	[deleted file]	blob \| history
helm/ocaml/getter/http_getter_md5.mli	[deleted file]	blob \| history
helm/ocaml/getter/http_getter_misc.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_misc.mli		diff \| blob \| history
helm/ocaml/getter/http_getter_storage.ml	[new file with mode: 0644]	blob
helm/ocaml/getter/http_getter_storage.mli	[new file with mode: 0644]	blob
helm/ocaml/getter/http_getter_types.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_wget.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_wget.mli		diff \| blob \| history
helm/ocaml/getter/mkindexes.pl	[new file with mode: 0755]	blob
helm/ocaml/getter/sample.conf.xml	[new file with mode: 0644]	blob
helm/ocaml/getter/test.ml		diff \| blob \| history
helm/ocaml/getter/tree.ml	[deleted file]	blob \| history
helm/ocaml/getter/tree.mli	[deleted file]	blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom