# HG changeset patch
# User wenzelm
# Date 850726696 -3600
# Node ID 6719b465198b8e2b162e2a1ec0f07844b829d09b
# Parent  d4164ea87229fa581eb61eb9106cdb2f2cc5d6a9
symbolinput - translate symbols into \<...> sequences;

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