Commit 0c6b9750 authored by Ralf Jung's avatar Ralf Jung
Browse files

add ability to pass additional flags to coqdoc

parent 3a28a3e3
......@@ -20,10 +20,12 @@ set -eo pipefail
## non-empty, submit timing information to coq-speed with the given project
## name and configuration string. The project names defaults to the
## repository name. Reqires the $TIMING_SECRET variable to be set.
## - $DOC_DIR, $DOC_BRANCH, $DOC_KEY: If $DOC_DIR is non-empty, run coqdoc and
## upload the results to the given directory. This only happens if the
## current branch is $DOC_BRANCH (defaults to master). Requires the $DOC_KEY
## variable to be set to the secret key for uploading.
## - $DOC_DIR, $DOC_BRANCH, $DOC_KEY, $DOC_OPTS: If $DOC_DIR is non-empty, run
## coqdoc and upload the results to the given directory. This only happens if
## the current branch is $DOC_BRANCH (defaults to master). Requires the
## $DOC_KEY variable to be set to the secret key for uploading. $DOC_OPTS can
## be set to pass additional flags to coqdoc (particularly useful for
## --external).
status "[buildjob] Using CI branch $(cd ci && git rev-parse --abbrev-ref HEAD) ($(cd ci && git rev-parse HEAD))"
......@@ -123,7 +125,7 @@ if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "$DOC_BRANCH" ]]; then
export GIT_SSH=$(readlink -e ci/ssh)
# Generate documentation and web server configuration
make html
COQDOCEXTRAFLAGS="$DOC_OPTS" make html
echo "DirectoryIndex toc.html" > html/.htaccess
# Upload documentation
rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment