From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 6 Feb 2004 12:28:58 +0000 (+0000)
Subject: textual term editor is now the default one
X-Git-Tag: V_0_2_3~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9b73cf28065e4ed65f4dadc3d4e519b453ae7a8;p=helm.git

textual term editor is now the default one
---

diff --git a/helm/ocaml/configure.ac b/helm/ocaml/configure.ac
index d8221cd51..36bcc703f 100644
--- a/helm/ocaml/configure.ac
+++ b/helm/ocaml/configure.ac
@@ -13,7 +13,7 @@ fi
 AC_ARG_WITH(term-editor,
 	      AS_HELP_STRING([--with-term-editor=(tex|textual)],
 			     [choose term editor (default is tex)]),
-	      [TERM_EDITOR=$withval], [TERM_EDITOR=tex])
+	      [TERM_EDITOR=$withval], [TERM_EDITOR=textual])
 if test $TERM_EDITOR = "tex"; then
   CHOSEN_TERM_EDITOR="include TexTermEditor"
 else