]> 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)
commit4f9820060bce92cfdb862b3c699e96c20c64a051
tree9927936b3c16952d229949195c1749022a11a47b
parent061e94c62f89915a193ebd342cefe4be1f8d2869
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
components/library/libraryDb.ml
components/library/libraryDb.mli
components/library/librarySync.ml