]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2833624) | 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)
commit19618ce16bb4a5fd2f7e88bfe9b5002511197faf
tree027a01a2098568fe73d9afb0ddd0fc5d1fecd415tree | snapshot
parent2833624d7e2bfea7525f75acd1e9284080eb6ea8commit | diff
Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.
helm/software/matita/matitadep.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.