]> matita.cs.unibo.it Git - helm.git/commitdiff
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)
 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


No differences found