From 95c956c8d0020ea1202d2c2ef354e2dcef641820 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 16 Feb 2004 09:43:55 +0000
Subject: [PATCH] do not use tex notation per default (used only by tex term
 editor)

---
 helm/ocaml/cic_disambiguation/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index ef4ff8cc2..ea516c526 100644
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -3,7 +3,8 @@ PACKAGE = cic_textual_parser2
 REQUIRES = \
 	helm-tactics helm-logger helm-cic_unification helm-cic_transformations \
 	ulex pxp camlp4.gramlib
-NOTATIONS = logic arit tex
+# NOTATIONS = logic arit tex
+NOTATIONS = logic arit
 INTERFACE_FILES = \
 	disambiguateTypes.mli \
 	disambiguateChoices.mli \
-- 
2.39.2