2 Commits

Include renames

Author	SHA1	Message	Date
David Lechner	2c4685f594	doc/main: add TAG make option ... This splits the Sphinx tag option from SPHINXOPTS. This allows us to specify the tag without having to remember to add -W and -t. It also fixes not being able to specify the tag with make.bat on Windows. While we are touching this, redundant SOURCEDIR uses are removed (main is already the default) and the .github/workflows/publish-ide-docs.yml script is fixed (ide directory no longer exists).	2021-08-30 12:14:34 -05:00
David Lechner	77605e8701	github: add workflow for publishing ide-docs package	2021-01-26 08:30:48 +01:00