]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 40bf8d7) | patch
Speeedup! (by caching)
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 22 Dec 2006 08:54:57 +0000 (08:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 22 Dec 2006 08:54:57 +0000 (08:54 +0000)
commitdf70518efb295cdce60a3df8098ac0a6eef2d9cf
tree536c99772506c14ce9f7da6ae8e885b1c67a435dtree | snapshot
parent40bf8d7dee174d96147a21856b3cebb59d1811eccommit | diff
Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.
matita/matitadep.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.