diff options
Diffstat (limited to 'explorer/upload-new.sh')
-rwxr-xr-x | explorer/upload-new.sh | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/explorer/upload-new.sh b/explorer/upload-new.sh new file mode 100755 index 0000000..7873aa2 --- /dev/null +++ b/explorer/upload-new.sh | |||
@@ -0,0 +1,16 @@ | |||
1 | #!/bin/bash | ||
2 | |||
3 | set -eu | ||
4 | set -o pipefail | ||
5 | |||
6 | commit="$(git rev-parse --short HEAD)" | ||
7 | |||
8 | [ -e "dest-$commit" ] && { | ||
9 | echo "Revision $commit may have already been uploaded. Delete the directory dest-$commit to force re-upload."; | ||
10 | exit 1 | ||
11 | } | ||
12 | |||
13 | ./generate.sh | ||
14 | mv dest "dest-$commit" | ||
15 | mcli cp --recursive --checksum sha256 dest-$commit/* s3-default-par/verified-dyn-lang-interp/$commit/theories/ | ||
16 | echo "Base URL (for \\rocqbaseurl): https://s3.fr-par.scw.cloud/verified-dyn-lang-interp/$commit/" | ||