diff --git a/.ci/.gitignore b/.ci/.gitignore new file mode 100644 index 0000000..1fd44ac --- /dev/null +++ b/.ci/.gitignore @@ -0,0 +1 @@ +/cached-shell diff --git a/.ci/cache-shell.sh b/.ci/cache-shell.sh new file mode 100755 index 0000000..b810324 --- /dev/null +++ b/.ci/cache-shell.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +source "$(dirname "${BASH_SOURCE[0]}")/common.sh" + +>&2 echo "Caching dev shell" +nix print-dev-env "${base}#" >"${cached_shell}" diff --git a/.ci/common.sh b/.ci/common.sh new file mode 100644 index 0000000..1c8d67c --- /dev/null +++ b/.ci/common.sh @@ -0,0 +1,7 @@ +# Use as: +# +# source "$(dirname "${BASH_SOURCE[0]}")/common.sh" + +set -euo pipefail +base="$(readlink -f $(dirname "${BASH_SOURCE[0]}")/..)" +cached_shell="${base}/.ci/cached-shell" diff --git a/.ci/run b/.ci/run new file mode 100755 index 0000000..67b60b0 --- /dev/null +++ b/.ci/run @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +source "$(dirname "${BASH_SOURCE[0]}")/common.sh" + +if [[ ! -f "${cached_shell}" ]]; then + >&2 echo "No cached shell in ${cached_shell}" + exit 1 +fi + +. "${cached_shell}" +exec "$@"