diff -r aa97eb904692 -r 590f9e3bf4d8 lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Mon Jan 11 18:45:46 1999 +0100
+++ b/lib/Tools/symbolinput	Tue Jan 12 12:17:53 1999 +0100
@@ -4,4 +4,7 @@
 #
 # DESCRIPTION: translate symbols into \<...> sequences
 
-exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
+#set by configure
+AUTO_PERL=perl
+
+exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"