diff options
Diffstat (limited to 'dist')
| -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" |