diff options
| author | Hendrik Tews | 2021-01-31 22:23:18 +0100 |
|---|---|---|
| committer | hendriktews | 2021-02-13 18:22:49 +0100 |
| commit | 7f52ca16c0ea17cc388c9c9d07e5c46c9e56ba14 (patch) | |
| tree | 69daab2747b855d95cab6f0b6b01289edec3e396 /coq/coq-compile-common.el | |
| parent | 89300b579aea2471448b8871b94c0e5982c7c059 (diff) | |
new github action for make magic
This action checks that
- make -C doc magic works
- the manual is currently up-to-date
The second check fails when somebody changes variable or function
documentation of something that appears in one of the manuals
without updating the manuals at the same time. Further, it fails
when emacs changes such that the function `texi-docstring-magic'
produces different output.
Diffstat (limited to 'coq/coq-compile-common.el')
0 files changed, 0 insertions, 0 deletions