Hanno Braun dc72a8ec58 Only run ci/after_success.sh, if a PR is merged ...

This should do the following:
1. Not run the code in `ci/after_success.sh` when a pull request is
   built, as the secret variable `GH_TOKEN` is not available then, which
   will cause a build error.
2. Run said script after a pull request has been merged to master, to
   automatically update documentation on gh-pages.

I know that 1. actually happens. I have no idea about 2.

2018-09-28 16:47:44 +02:00

..

after_success.sh

Only run ci/after_success.sh, if a PR is merged

2018-09-28 16:47:44 +02:00

install.sh

replace uses of ! with Void

2018-05-11 14:01:18 +02:00

script.sh

replace uses of ! with Void

2018-05-11 14:01:18 +02:00