aboutsummaryrefslogtreecommitdiffstats
#!/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/"