diff -r d4164ea87229 -r 6719b465198b lib/Tools/symbolinput
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/symbolinput	Mon Dec 16 09:58:16 1996 +0100
@@ -0,0 +1,17 @@
+#!/bin/bash -norc
+#
+# $Id$
+#
+# DESCRIPTION: translate symbols into \<...> sequences
+#
+# NOTE: If perl is unavailable we simply fall back on cat!
+
+
+PERL=$(type -path perl)
+
+if [ -z "$PERL" ]
+then
+  exec cat "$@"
+else
+  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
+fi