blasting a bunch of builds

mtzguido · Jan 11, 2025 · d376aad · d376aad
1 parent dca19d3
commit d376aad
Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
@@ -11,7 +11,7 @@ name: F* nightly build
 
 on:
   schedule:
-    - cron: '0 * * * *'
+    - cron: '*/10 * * * *'
   workflow_dispatch:
 
 jobs:
@@ -45,7 +45,7 @@ jobs:
 
           # We push nightly builds to a different repo (same org)
           REPO="${{github.repository}}-nightly"
-          TAG=nightly-$(date -I)
+          TAG=nightly-$(date -I)-$((RANDOM))
 
           # Create tag
           git tag $TAG ${{github.sha}}

diff --git a/.scripts/mk-package.sh b/.scripts/mk-package.sh
@@ -35,7 +35,7 @@ case $FSTAR_PACKAGE_FORMAT in
     TGT="$ARCHIVE.zip"
     TGT="$(realpath "$TGT")"
     # Github actions runner do not have 'zip'
-    if wwwhich zip; then
+    if which zip; then
       zip -q -r -9 "$TGT" .
     elif which 7z; then
       pushd "$PREFIX"