aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-10-07 15:07:27 +0000
committerGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-10-07 15:07:27 +0000
commit334cbcdffd811135cbc282ef1eace1bc69b0ccbd (patch)
treebc37c15c6288677d0d3b07b12c75e55ffc1d80df /config
parent4eafa1c201eb851c98273d6d78377ce32586a658 (diff)
TeX input method is now supported upstream
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template3
1 files changed, 0 insertions, 3 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 8fb9e48c3..8000c6169 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -139,9 +139,6 @@ STRIP=STRIPCOMMAND
# CoqIde (no/byte/opt)
HASCOQIDE=COQIDEOPT
-# IM files
-UIMSCRIPTDIR=UIMSCRIPTPATH
-
# Defining REVISION
CHECKEDOUT=CHECKEDOUTSOURCETREE