]> matita.cs.unibo.it Git - helm.git/commit
remove_obj is now much faster:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 30 Oct 2006 16:40:19 +0000 (16:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 30 Oct 2006 16:40:19 +0000 (16:40 +0000)
commit4b98f68b964c9f87868c445e794bc745a99d5b17
treedf478baefaf86cf2c4c81d79622cbf47d9c72322
parent2cd3e5e157c86a07666eb7501b5050cbafdfe6b1
remove_obj is now much faster:
 1. the code was utterly messy, trying to remove from the DB files and
    to remove from disk #xpointer uris.
 2. LIKE substituted by =
 3. added QUICK and LOW_PRIORITY to the DELETE statement
 4. removed unuseful and unused debugging code that used to slow down every
    deletion
helm/software/components/library/libraryDb.ml
helm/software/components/library/libraryDb.mli
helm/software/components/library/librarySync.ml