diff options
Diffstat (limited to 'checker')
-rw-r--r-- | checker/include | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/include b/checker/include index 09bf2826c..da0346359 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp4";; #directory "+camlp5";; #load "unix.cma";; |