obsolete;

--- a/lib/Tools/symbolinput	Mon Dec 10 18:52:15 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# DESCRIPTION: translate symbols into \<...> sequences
-
-#set by configure
-AUTO_PERL=perl
-
-exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"