32ea0508cf
_build/github-deploy.sh: Fix exit code on conflicting remote commit
10 years ago
8c24e32f10
Build scripts: Fix formatting
10 years ago
26d7d2f68e
Build scripts: Fix formatting
10 years ago
cd0e0f706f
Build scripts: Git identity must be configured before committing
10 years ago
92026a3bd0
Add static shields.io badge generator
10 years ago
0198d827bf
Build scripts: Add file comments
10 years ago
c88a26beff
phpDocs auto deployment: Set default push strategy to simple
10 years ago
fe10bca56b
phpDocs auto deployment: Fix output formatting
10 years ago
76f243f925
Refactor phpDoc deployment
...
This should prevent empty phpDoc updates like 55b4a2b
10 years ago
1dc410425f
Isolate build-related files from source
...
* [Changed] rename `phpcs.xml` -> `.phpcs.xml`
* [Changed] rename `build/` dir -> `_build/`
* [Changed] update paths in `.gitignore`
* [Changed] update paths in `.travis.yml`
* [Changed] update paths in `.sh` scripts
10 years ago
45dcf32fa7
phpDocs auto deployment: Support pull requests in a safe environment
10 years ago
5af160c31d
phpDocs auto deployment: Use $GITHUB_OAUTH_TOKEN to determine latest commit
10 years ago
17dbc4cf18
phpDocs auto deployment: Cleanup
10 years ago
236ae43dab
phpDocs auto deployment: Fix deployment of branches
10 years ago
c198333de7
Improve phpDocs auto-generation
10 years ago
728873c5a4
build/deploy-phpdoc.sh: Fix credentials
10 years ago
3c68095075
Improve phpDocs auto-generation
10 years ago
3852585ba0
Improve phpDocs auto-generation
10 years ago
9a46033141
Improve phpDocs auto-generation
10 years ago
c9387610f3
Auto-generate phpDoc when committing to master
10 years ago
9712ae2a97
Fix permissions of build/deploy-phpdoc.sh
10 years ago
7f4ad75245
Refactor phpDoc auto-deployment
10 years ago
c3b908939f
update deploy-phpdoc.sh for auto docs
10 years ago
bf2a9622db
Update deploy script
...
* [Changed] move everything inside /build/ directory
* [Changed] use absolute file paths in script
* [Changed] copy docs to both the release number and master dirs
Implement @PhrozenByte 's suggestions.
* [Changed] use `$GITHUB_OAUTH_TOKEN` instead of `$GITHUB_TOKEN`
10 years ago
Daniel Rudolf
theshka