# HG changeset patch
# User wenzelm
# Date 855249779 -3600
# Node ID 9d910f3681d020638b1c554a63f2d8dd0943286a
# Parent  b472d703fa06062d0c66ed2a74982e7f03385441
now falls back on ucat instead of cat;

diff -r b472d703fa06 -r 9d910f3681d0 lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Thu Feb 06 18:22:21 1997 +0100
+++ b/lib/Tools/symbolinput	Thu Feb 06 18:22:59 1997 +0100
@@ -4,14 +4,14 @@
 #
 # DESCRIPTION: translate symbols into \<...> sequences
 #
-# NOTE: If perl is unavailable we simply fall back on cat!
+# NOTE: If perl is unavailable we simply fall back on ucat!
 
 
 PERL=$(type -path perl)
 
 if [ -z "$PERL" ]
 then
-  exec cat "$@"
+  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
 else
   exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
 fi