From b60906cc3ee3f994babf9cceff2971bd03485f2f Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 22 Jan 2018 12:45:49 -0800
Subject: Change references to CAMLP4 to CAMLP5 to be more accurate since we no
 longer use camlp4.

---
 dev/core.dbg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/core.dbg')

diff --git a/dev/core.dbg b/dev/core.dbg
index 00a4355a48..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
-- 
cgit v1.2.3