From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Oct 2002 08:51:51 +0000 (+0000)
Subject: - matql_interpreter_galax branch removed once and for ever
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b9b3b6c5a9f818019aaeac0876ce0874e7a3651d;p=helm.git

- matql_interpreter_galax branch removed once and for ever
- added the dependency to natile-galax. You need to add
  /projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib
  to your OCAMLPATH to make it compile again.
---

diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore
index 04c50217e..18745fc01 100644
--- a/helm/ocaml/.cvsignore
+++ b/helm/ocaml/.cvsignore
@@ -10,7 +10,6 @@ META.helm-cic_proof_checking
 META.helm-cic_textual_parser
 META.helm-cic_unification
 META.helm-mathql_interpreter
-META.helm-mathql_interpreter_galax
 META.helm-mathql
 Makefile
 Makefile.common
diff --git a/helm/ocaml/META.helm-mathql_interpreter.src b/helm/ocaml/META.helm-mathql_interpreter.src
index 8cc8c445c..7247741fd 100644
--- a/helm/ocaml/META.helm-mathql_interpreter.src
+++ b/helm/ocaml/META.helm-mathql_interpreter.src
@@ -1,4 +1,4 @@
-requires="helm-urimanager postgres"
+requires="helm-urimanager postgres natile-galax"
 version="0.0.1"
 archive(byte)="mathql_interpreter.cma"
 archive(native)="mathql_interpreter.cmxa"
diff --git a/helm/ocaml/META.helm-mathql_interpreter_galax.src b/helm/ocaml/META.helm-mathql_interpreter_galax.src
deleted file mode 100644
index 41c999cee..000000000
--- a/helm/ocaml/META.helm-mathql_interpreter_galax.src
+++ /dev/null
@@ -1,4 +0,0 @@
-requires="helm-urimanager num natile-galax"
-version="0.0.1"
-archive(byte)="mathql_interpreter_galax.cma"
-archive(native)="mathql_interpreter_galax.cmxa"