src/Tools/Demo/etc/settings
author Fabian Huch <huch@in.tum.de>
Fri, 07 Jun 2024 15:47:19 +0200
changeset 80281 17d2f775907a
parent 79058 f13390b2c1ee
permissions -rw-r--r--
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;

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

ISABELLE_DEMO_HOME="$COMPONENT"