aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Expand)AuthorAge
* Merge PR #7219: merge script support https + typos in docGravatar Maxime Dénès2018-04-19
|\
* | pre-commit : do not fail miserably if git config has `apply.whitespace = fix`Gravatar Pierre Letouzey2018-04-17
| * merge script support https + typos in docGravatar Pierre Courtieu2018-04-11
|/
* Merge script: adds a way for confirmation to expect a newline.Gravatar Théo Zimmermann2018-04-09
* Add sanity check in merge script: local branch is up-to-date.Gravatar Théo Zimmermann2018-04-09
* Document requirement to have git >= 2.7 to use the merge script.Gravatar Théo Zimmermann2018-04-08
* Merge script does not warn when the remote is set to HTTPS.Gravatar Théo Zimmermann2018-04-08
* Merge script: use fetch URL for the remote.Gravatar Théo Zimmermann2018-04-08
* Improve shell scriptsGravatar zapashcanon2018-04-05
* merge-pr.sh: cache github API callsGravatar Gaëtan Gilbert2018-04-03
* pre-commit: verify user overlay extensions (must be .sh).Gravatar Gaëtan Gilbert2018-03-31
* improve merge-pr scriptGravatar Enrico Tassi2018-03-23
* Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\
* \ Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\ \
| | * coqdev.el: add space at the end of compile-commandGravatar Gaëtan Gilbert2018-02-21
| |/ |/|
* | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \
| * | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| * | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| * | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| * | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
* | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \
| | * | Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | * | coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | * pre-commit: nicer messagesGravatar Gaëtan Gilbert2018-02-08
| | | * pre-commit: fail gracefully if fixing whitespace removes all changesGravatar Gaëtan Gilbert2018-02-08
| | | * pre-commit: add files after fixing ending newlines.Gravatar Gaëtan Gilbert2018-02-08
| | | * Have the pre-commit hook also fix end-of-file nlGravatar Jason Gross2018-02-08
| | | * Auto-create .git/hooks/pre-commit on ./configureGravatar Jason Gross2018-02-08
| | | * pre-commit hook: fix whitespace error detectionGravatar Gaëtan Gilbert2018-02-08
| | | * A pre-commit hook to magically fix whitespace issues.Gravatar Gaëtan Gilbert2018-02-08
* | | | Use travis_retry on apt-get updateGravatar Jason Gross2018-01-23
| |_|/ |/| |
* | | Merge PR #6568: Cleanup scriptsGravatar Maxime Dénès2018-01-23
|\ \ \
| * | | merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
| * | | Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
| * | | Simplify logic and streamline lint-repository.shGravatar Gaëtan Gilbert2018-01-16
* | | | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelGravatar Maxime Dénès2018-01-10
|\ \ \ \
| | | * | [Backport script] Check .mli files are not changed.Gravatar Théo Zimmermann2018-01-09
| |_|/ / |/| | |
| * | | github-check-prs.py: print PR URLs when needed.Gravatar Gaëtan Gilbert2018-01-08
| * | | github-check-prs.py: Strip spaces from token from command lineGravatar Gaëtan Gilbert2018-01-08
| * | | github-check-prs.py: command line option to get token from a fileGravatar Gaëtan Gilbert2018-01-08
| | | * Remove dir-locals and ship suggested helper hooks instead.Gravatar Gaëtan Gilbert2018-01-06
| | |/
| * | Expound on dependencies for github-check-prs.pyGravatar Gaëtan Gilbert2017-12-30
| * | Python script checking missing/unnecessary [needs: rebase] labelGravatar Gaëtan Gilbert2017-12-30
| |/
* / Update backport script for more control.Gravatar Théo Zimmermann2017-12-24
|/
* Fix usage comment.Gravatar Théo Zimmermann2017-11-29
* This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
* Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
* Add PR backport script.Gravatar Théo Zimmermann2017-11-28
* Add PR merge script.Gravatar Maxime Dénès2017-11-28
* Linter: do not lint untracked files.Gravatar Gaëtan Gilbert2017-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 10:03:55 +0000