Check the syntax of reStructuredText files during CI#112

Merged

UNAA008 merged 17 commits intomasterfrom branch/2023-01-13/rst-check

Feb 10, 2023

+124-20

Commits on Jan 14, 2023

Adding a GitHub CI workflow to check the syntax of reStructuredText files.
rptb1
committed
Suppress Travis CI on branch/2023-01-13/rst-check for faster testing of GitHub CI.
rptb1
committed
Run checking steps even if other steps fail.
rptb1
committed
Moving checking to its own script so it can be used at the command line, which also simplifies the GitHub workflow.
rptb1
committed
Refining pruning rules for command-line use.
rptb1
committed
Fixing basic reStructuredText syntax and reference errors found by tool/checkrst.
rptb1
committed
Improving the naming so that results are clearer in GitHub output.
rptb1
committed
Fixing warnings found by shellcheck.
rptb1
committed
Fixing duplicate tag design.mps.config.var introduced in commit 533f4fa
rptb1
committed
Oops, forgot to fix up the RST ref in commit caa7a60
rptb1
committed
Fixing duplicate tags introduced by e9841d2 as a consequence of b0433b3
rptb1
committed
Fixing duplicate tag design.mps.arena.tract.field.base. Looks like a copy-paste error.
rptb1
committed
Fixing duplicate tag design.mps.prmc.if.init.thread. Looks like a copy-paste error.
rptb1
committed

Commits on Jan 15, 2023

Commits on Jan 17, 2023

Clarifying that this checks the MPS source tree, not the MPS. Signing.
rptb1
committed

Commits on Jan 25, 2023

Linking comment about smushed document to GitHub issue 128 <#128 > that logs it.
rptb1
committed