From 97fb17dfe5e6f1a8e720048d1a02309ace423051 Mon Sep 17 00:00:00 2001
From: Alessandro Pignotti <a.pignotti@sssup.it>
Date: Tue, 15 Oct 2024 12:25:25 +0200
Subject: [PATCH] GH: Fix pages deployment

---
 .github/workflows/deploy.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
index 38e77ad..b8b4fb8 100644
--- a/.github/workflows/deploy.yml
+++ b/.github/workflows/deploy.yml
@@ -190,7 +190,7 @@ jobs:
           WEBVM_MODE=github npm run build
 
       # Move required files for gh-pages deployment to the deployment directory $DEPLOY_DIR.
-      - run: sudo mv build $DEPLOY_DIR
+      - run: sudo mv build/* $DEPLOY_DIR/
 
       # We generate index.list files for our httpfs to function properly.
       - name: make index.list