Merge branch 'master' into optimized-defaults

runtimeverification · Aug 24, 2023 · b047ec3 · b047ec3
2 parents 9125462 + ba06470
commit b047ec3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -153,7 +153,7 @@ jobs:
           npm run build-sitemap
           cd -
           mv web/public_content ./
-          rm -rf $(find . -maxdepth 1 -not -name public_content -a -not -name .git -a -not -path . -a -not -path .. -a -not -name CNAME)
+          rm -rf $(find . -maxdepth 1 -not -name public_content -a -not -name .git -a -not -name .gitmodules -a -not -path . -a -not -path .. -a -not -name CNAME)
           mv public_content/* ./
           rm -rf public_content
           git add ./