From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- explorer/upload-new.sh | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100755 explorer/upload-new.sh (limited to 'explorer/upload-new.sh') 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 @@ +#!/bin/bash + +set -eu +set -o pipefail + +commit="$(git rev-parse --short HEAD)" + +[ -e "dest-$commit" ] && { + echo "Revision $commit may have already been uploaded. Delete the directory dest-$commit to force re-upload."; + exit 1 +} + +./generate.sh +mv dest "dest-$commit" +mcli cp --recursive --checksum sha256 dest-$commit/* s3-default-par/verified-dyn-lang-interp/$commit/theories/ +echo "Base URL (for \\rocqbaseurl): https://s3.fr-par.scw.cloud/verified-dyn-lang-interp/$commit/" -- cgit v1.2.3