]> matita.cs.unibo.it Git - helm.git/commit
allow to switch profiling on and off on the fly
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 9 Apr 2008 11:59:49 +0000 (11:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 9 Apr 2008 11:59:49 +0000 (11:59 +0000)
commit4b5527a6ccbe73ada47f903292959ed3dde3b5c6
tree2e7ef2d41351e7ff0bc24c56ece6244b81f042bc
parent497fcd1fe028781bcb3853044dc787d83fa8d1a9
allow to switch profiling on and off on the fly
helm/software/components/extlib/hExtlib.ml
helm/software/components/extlib/hExtlib.mli