Also regenerate doc when workflow is modified

flintlib · Oct 9, 2023 · 9788289 · 9788289
1 parent 40d1a53
commit 9788289
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -21,7 +21,7 @@ jobs:
       - name: "Check for changes in documentation"
         id: check_doc_changes
         run: |
-          if test -z "$(git diff --name-only HEAD~1..HEAD -- doc/)";
+          if test -z "$(git diff --name-only HEAD~1..HEAD -- doc/ .github/workflows/docs.yml)";
           then
             echo "No changes in doc/"
             echo "diff=false" >> $GITHUB_OUTPUT