diff options
Diffstat (limited to 'dev/checker.dbg')
| -rw-r--r-- | dev/checker.dbg | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/dev/checker.dbg b/dev/checker.dbg deleted file mode 100644 index b5b7f0e6d3..0000000000 --- a/dev/checker.dbg +++ /dev/null @@ -1,7 +0,0 @@ -load_printer threads.cma -load_printer str.cma -load_printer clib.cma -load_printer dynlink.cma -load_printer config.cma -load_printer lib.cma -load_printer check.cma |