diff --git a/docs/test_documentation.sh b/docs/test_documentation.sh new file mode 100755 index 0000000000000000000000000000000000000000..b19664ad2af79404c5367016773632ca5e164665 --- /dev/null +++ b/docs/test_documentation.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +docker run -it --rm -v $(pwd):/docs sphinxdoc/sphinx:latest /bin/bash -c \ +"pip install sphinx_rtd_theme myst-parser;cd docs;make html" + +docker run -it --rm -v $(pwd):/gap jdkato/vale:latest --config="/gap/vale/.vale.ini" sync +docker run -it --rm -v $(pwd):/gap jdkato/vale:latest --config="/gap/vale/.vale.ini" /gap/build/html/_sources/