]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4279f25) | patch
New: stylesheets are now partially cached (i.e. all the stylesheets which
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 29 Apr 2003 16:14:25 +0000 (16:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 29 Apr 2003 16:14:25 +0000 (16:14 +0000)
commit1d4f3c9c4b5241c085b1af4fd7c2bf58585532a7
treeae43b7e973cd1d422ff54bada56073ca47a975cdtree | snapshot
parent4279f2559d951de4f7bcd6e63dc35052e7f19c51commit | diff
New: stylesheets are now partially cached (i.e. all the stylesheets which
are applied using an empty list of props are now precompiled only when
added or reloaded). See bug #75.
helm/uwobo/uwobo_engine.ml diff | blob | history
helm/uwobo/uwobo_styles.ml diff | blob | history
helm/uwobo/uwobo_styles.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.