src/Tools/GraphBrowser/etc/settings
author wenzelm
Thu, 10 Aug 2023 19:42:21 +0200
changeset 78506 14da1177d1c3
parent 74011 1d366486a812
permissions -rw-r--r--
more informative error;

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

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