diff options
| -rw-r--r-- | Doc/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Doc/Makefile b/Doc/Makefile index a774aad..3c7196e 100644 --- a/Doc/Makefile +++ b/Doc/Makefile @@ -186,6 +186,7 @@ serve: autobuild-dev: make update make dist SPHINXOPTS='-A daily=1 -A versionswitcher=1' + -make suspicious # for quick rebuilds (HTML only) autobuild-html: |