#!/bin/bash # # $Id$ # # DESCRIPTION: translate symbols into \<...> sequences exec perl -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"