src/Tools/Code/etc/settings
author wenzelm
Wed, 12 Sep 2012 13:21:33 +0200
changeset 49321 a48f9bbbe720
parent 41952 c7297638599b
permissions -rw-r--r--
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);

# -*- shell-script -*- :mode=shellscript:

ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"