From 1bd503d31db62ec1f4b1dfb416c11615f3af7248 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sat, 24 Jan 2004 12:35:09 +0000
Subject: [PATCH] .in version of "configuration" modules

---
 helm/gTopLevel/chosenTermEditor.ml                         | 4 ----
 helm/gTopLevel/chosenTermEditor.ml.in                      | 1 +
 helm/gTopLevel/chosenTransformer.ml                        | 2 --
 helm/gTopLevel/chosenTransformer.ml.in                     | 1 +
 ...{disambiguatingParser.ml => disambiguatingParser.ml.in} | 7 ++-----
 5 files changed, 4 insertions(+), 11 deletions(-)
 delete mode 100644 helm/gTopLevel/chosenTermEditor.ml
 create mode 100644 helm/gTopLevel/chosenTermEditor.ml.in
 delete mode 100644 helm/gTopLevel/chosenTransformer.ml
 create mode 100644 helm/gTopLevel/chosenTransformer.ml.in
 rename helm/gTopLevel/{disambiguatingParser.ml => disambiguatingParser.ml.in} (96%)

diff --git a/helm/gTopLevel/chosenTermEditor.ml b/helm/gTopLevel/chosenTermEditor.ml
deleted file mode 100644
index 25dcfd2e5..000000000
--- a/helm/gTopLevel/chosenTermEditor.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-include TermEditor
-(*
-include TexTermEditor
-*)
diff --git a/helm/gTopLevel/chosenTermEditor.ml.in b/helm/gTopLevel/chosenTermEditor.ml.in
new file mode 100644
index 000000000..d501e8d06
--- /dev/null
+++ b/helm/gTopLevel/chosenTermEditor.ml.in
@@ -0,0 +1 @@
+@CHOSEN_TERM_EDITOR@
diff --git a/helm/gTopLevel/chosenTransformer.ml b/helm/gTopLevel/chosenTransformer.ml
deleted file mode 100644
index 85e27049a..000000000
--- a/helm/gTopLevel/chosenTransformer.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-(* include ApplyStylesheets *)
-include ApplyTransformation
diff --git a/helm/gTopLevel/chosenTransformer.ml.in b/helm/gTopLevel/chosenTransformer.ml.in
new file mode 100644
index 000000000..e81993ec3
--- /dev/null
+++ b/helm/gTopLevel/chosenTransformer.ml.in
@@ -0,0 +1 @@
+@CHOSEN_TRANSFORMER@
diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml.in
similarity index 96%
rename from helm/gTopLevel/disambiguatingParser.ml
rename to helm/gTopLevel/disambiguatingParser.ml.in
index eb89b1170..25953b502 100644
--- a/helm/gTopLevel/disambiguatingParser.ml
+++ b/helm/gTopLevel/disambiguatingParser.ml.in
@@ -98,8 +98,5 @@ module CSCTexDisambiguatingParser =
    end
  end
 
-include AndreaAndZackDisambiguatingParser
-(*
-include CSCTextualDisambiguatingParser
-include CSCTexDisambiguatingParser
-*)
+@CHOSEN_TERM_PARSER@
+
-- 
2.39.2