ci: Remove comment with script snippet

Signed-off-by: Nick Spinale <[email protected]>
seL4 · Oct 7, 2023 · 02e55cd · 02e55cd
1 parent 5a266c8
commit 02e55cd
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/.github/workflows/push.yaml b/.github/workflows/push.yaml
@@ -141,6 +141,3 @@ jobs:
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v2
-
-# For debugging and monitoring disk usage:
-# (make foo && df -h) || (df -h && false)