aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq-tex.ml4 (renamed from tools/coq-tex.ml)0
-rw-r--r--tools/coq_makefile.ml4 (renamed from tools/coq_makefile.ml)0
2 files changed, 0 insertions, 0 deletions
diff --git a/tools/coq-tex.ml b/tools/coq-tex.ml4
index 541777d6e4..541777d6e4 100644
--- a/tools/coq-tex.ml
+++ b/tools/coq-tex.ml4
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml4
index 613257c685..613257c685 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml4