]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 55ec392) | patch
I do not know why, but
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Jun 2007 13:20:21 +0000 (13:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Jun 2007 13:20:21 +0000 (13:20 +0000)
commit798e85cb6d55d80d988f91e6289e4041e95ad2e4
treed0f60eef963fa5a3f6f58a0817a63cb3bf7feed5tree | snapshot
parent55ec3926f6fbb5dba13705659fe94d0db38b2666commit | diff
I do not know why, but
(Helm_registry.get_list Helm_registry.string "matita.includes")
is extremely slow! Removing it from the inner loop really improves performances!
helm/software/matita/matitaWiki.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.