aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Expand)AuthorAge
* Merge PR #8054: [dev] Autogenerate OCaml dev files.Gravatar Enrico Tassi2018-07-18
|\
* | Only check overlay extensions on git-tracked filesGravatar Jason Gross2018-07-16
| * [dev] Autogenerate OCaml dev files.Gravatar Emilio Jesus Gallego Arias2018-07-12
|/
* Add new options --no-conflict and --no-signature-check to backport script.Gravatar Théo Zimmermann2018-07-10
* [merge script] Check if the CI that was run is outdated.Gravatar Théo Zimmermann2018-06-09
* [doc] Add an ELisp snippet to insert Sphinx roles and quotesGravatar Clément Pit-Claudel2018-05-15
* Merge PR #7170: Script to identify the code owner for given filesGravatar Maxime Dénès2018-05-14
|\
* \ Merge PR #7337: dir-locals: add bug-reference-mode variablesGravatar Emilio Jesus Gallego Arias2018-05-14
|\ \
| * | coqdev.el: add bug-reference-mode variablesGravatar Gaëtan Gilbert2018-05-11
* | | use at least 6 Xs in mktemp filename templatesGravatar Sven M. Hallberg2018-05-09
|/ /
| * Add check-owners-pr.sh wrapper around check-ownersGravatar Gaëtan Gilbert2018-04-26
* | 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
| * check-owners.sh: add --show-patterns and --owner optionsGravatar Gaëtan Gilbert2018-04-04
| * Script to identify the code owner for given filesGravatar Gaëtan Gilbert2018-04-04
* | 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
| |_|/ / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 18:36:37 +0000