Make sure the docs/_include folder exists

Otherwise you get confusing errors in CI
YaelDillies · Dec 12, 2023 · 83d4a30 · 83d4a30
1 parent 475375f
commit 83d4a30
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -37,6 +37,7 @@ jobs:
         run: |
           grep -r --exclude-dir=ExampleSheets --files-without-match 'import LeanCamCombi' LeanCamCombi | sort > 1.txt
           grep -r --exclude-dir=ExampleSheets --files-with-match 'sorry' LeanCamCombi | sort > 2.txt
+          mkdir -p docs/_includes
           comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanCamCombi\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
           rm 1.txt 2.txt