From aa151dbc7aa501bac78b835a80f9a25c5316d2dc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 8 Nov 2018 03:11:06 +0100
Subject: [camlp5] Remove dependency on camlp5.

---
 dev/base_include | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index d2e8f6d092..48feeec147 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -8,6 +8,7 @@
 #directory "toplevel";;
 #directory "library";;
 #directory "kernel";;
+#directory "gramlib";;
 #directory "engine";;
 #directory "pretyping";;
 #directory "lib";;
@@ -18,8 +19,6 @@
 #directory "stm";;
 #directory "vernac";;
 
-#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
-
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
-- 
cgit v1.2.3