lib/Tools/caddy
author wenzelm
Thu, 12 Jun 2025 12:44:47 +0200
changeset 82695 d93ead9ac6df
parent 82615 3e20da339306
permissions -rwxr-xr-x
discontinue old infixes;
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