diff options
Diffstat (limited to 'dev/core.dbg')
| -rw-r--r-- | dev/core.dbg | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/core.dbg b/dev/core.dbg index 18e82c352c..57c136900d 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,4 +1,4 @@ -source camlp4.dbg +source camlp5.dbg load_printer threads.cma load_printer str.cma load_printer clib.cma @@ -17,5 +17,4 @@ load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer intf.cma -load_printer API.cma load_printer ltac_plugin.cmo |