diff options
| author | 1138-4EB <1138-4EB@users.noreply.github.com> | 2019-01-06 16:56:41 +0100 |
|---|---|---|
| committer | tgingold <tgingold@users.noreply.github.com> | 2019-01-06 16:56:41 +0100 |
| commit | 7021fba68ae037edb0899e137785cbe3f5d9ac35 (patch) | |
| tree | f6b1855db03594dddffbc52962b151fd3084d0d6 /dist/travis | |
| parent | 612a472d6c9f01d7b361f7baec15fb52f24654ef (diff) | |
| download | ghdl-7021fba68ae037edb0899e137785cbe3f5d9ac35.tar.gz ghdl-7021fba68ae037edb0899e137785cbe3f5d9ac35.tar.bz2 ghdl-7021fba68ae037edb0899e137785cbe3f5d9ac35.zip | |
Add man pages job to travis (#733)
* add man pages job to travis
Diffstat (limited to 'dist/travis')
| -rwxr-xr-x | dist/travis/man.sh | 13 | ||||
| -rwxr-xr-x | dist/travis/travis-ci.sh | 2 |
2 files changed, 14 insertions, 1 deletions
diff --git a/dist/travis/man.sh b/dist/travis/man.sh new file mode 100755 index 000000000..ab00cb4c9 --- /dev/null +++ b/dist/travis/man.sh @@ -0,0 +1,13 @@ +#! /bin/bash + +rm -rf doc/_build/man/* + +set -e + +docker run --rm -it \ + -v /$(pwd):/src \ + -w //src/doc \ + btdi/sphinx:py2-featured \ + sh -c "sphinx-build -T -b man . ./_build/man" + +nroff -man doc/_build/man/ghdl.1 diff --git a/dist/travis/travis-ci.sh b/dist/travis/travis-ci.sh index 628acceaf..0dda09931 100755 --- a/dist/travis/travis-ci.sh +++ b/dist/travis/travis-ci.sh @@ -29,6 +29,7 @@ scriptdir=$(dirname $0) . "$scriptdir/../ansi_color.sh" #disable_color + # Display env (to debug) echo -en "travis_fold:start:travis_env\r" @@ -47,7 +48,6 @@ echo "travis_fold:start:fetch" # The command 'git describe' (used for version) needs the history. Get it. # But the following command fails if the repository is complete. git fetch --unshallow || true - echo "travis_fold:end:fetch" |