lib/Tools/caddy
author wenzelm
Sun, 01 Jun 2025 17:06:33 +0200
changeset 82680 f7f8bb1c28ce
parent 82615 3e20da339306
permissions -rwxr-xr-x
obsolete (see 22d65e375c01);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
82615
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     2
#
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     3
# Author: Makarius
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     4
#
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: invoke caddy within the Isabelle environment
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     6
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     7
if [ -z "$ISABELLE_CADDY" ]; then
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     8
  echo "Missing Caddy installation: need to run \"isabelle caddy_setup\" first" >&2
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
     9
  exit 2
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
    10
else
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
    11
  exec "$ISABELLE_CADDY" "$@"
3e20da339306 provide "isabelle caddy_setup" and "isabelle caddy";
wenzelm
parents:
diff changeset
    12
fi