author | wenzelm |
Mon, 10 Dec 2001 19:14:56 +0100 | |
changeset 12456 | 95bed2b95448 |
parent 12455 | 7633c0fad9bd |
child 12457 | cbfc53e45476 |
lib/Tools/symbolinput | file | annotate | diff | comparison | revisions |
--- 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" "$@"