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