projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Remove some unneeded code that was slowing down the run function.
[tatoo.git]
/
include
/
debug.ml
diff --git
a/include/debug.ml
b/include/debug.ml
index
5a51787
..
1fd4f8b
100644
(file)
--- a/
include/debug.ml
+++ b/
include/debug.ml
@@
-4,9
+4,11
@@
DEFINE DEBUG__ML__
IFDEF DEBUG
THEN
- DEFINE DBG(e) = (e)
+ let msg x = Logger.msg `DEBUG x
+ DEFINE DEBUG(e) = (e)
ELSE
- DEFINE DBG(e) = ()
+ let msg x = ()
+ DEFINE DEBUG(e) = ()
END