Add check to docs CI whether Spicy docs are up to date.

This commit is contained in:
Robin Sommer 2023-09-21 09:51:21 +02:00
parent 21d6cf8190
commit 08d8dd51ca
No known key found for this signature in database
GPG key ID: D8187293B3FFE5D0

View file

@ -84,6 +84,9 @@ jobs:
- name: Build - name: Build
run: cd build && make -j $(nproc) run: cd build && make -j $(nproc)
- name: Check Spicy docs
run: cd doc && make check-spicy-docs
- name: Generate Docs - name: Generate Docs
run: | run: |
git config --global user.name zeek-bot git config --global user.name zeek-bot