aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Collapse)Author
2018-05-15[doc] Add an ELisp snippet to insert Sphinx roles and quotesClément Pit-Claudel
2018-05-14Merge PR #7170: Script to identify the code owner for given filesMaxime Dénès
2018-05-14Merge PR #7337: dir-locals: add bug-reference-mode variablesEmilio Jesus Gallego Arias
2018-05-11coqdev.el: add bug-reference-mode variablesGaëtan Gilbert
2018-05-09use at least 6 Xs in mktemp filename templatesSven M. Hallberg
OpenBSD mktemp fails with an error otherwise.
2018-04-26Add check-owners-pr.sh wrapper around check-ownersGaëtan Gilbert
``` $ dev/tools/check-owners-pr.sh 6809 --show-patterns --owner '@MSoegtropIMC' remote: Counting objects: 93, done. remote: Compressing objects: 100% (3/3), done. remote: Total 93 (delta 47), reused 50 (delta 47), pack-reused 43 Unpacking objects: 100% (93/93), done. From github.com:coq/coq * branch refs/pull/6809/head -> FETCH_HEAD * branch master -> FETCH_HEAD /dev/build/windows: @MSoegtropIMC ```
2018-04-19Merge PR #7219: merge script support https + typos in docMaxime Dénès
2018-04-17pre-commit : do not fail miserably if git config has `apply.whitespace = fix`Pierre Letouzey
Having `--whitespace=` on all `git apply` in this script should make it insensitive to user setup in `~/.gitconfig`, at least `[apply] whitespace = fix`. Note that even this way, this script remains hugely fragile and non mature, and would better *not* be set by default for everybody.
2018-04-11merge script support https + typos in docPierre Courtieu
2018-04-09Merge script: adds a way for confirmation to expect a newline.Théo Zimmermann
This fulfils Gaetan's wish.
2018-04-09Add sanity check in merge script: local branch is up-to-date.Théo Zimmermann
In case the local branch is ahead of upstream, we only print a warning because it could be that we are merging several PRs in a row.
2018-04-08Document requirement to have git >= 2.7 to use the merge script.Théo Zimmermann
As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
2018-04-08Merge script does not warn when the remote is set to HTTPS.Théo Zimmermann
This should solve Emilio's problem.
2018-04-08Merge script: use fetch URL for the remote.Théo Zimmermann
In case the push URL has been overriden to make it fetch-only.
2018-04-05Improve shell scriptszapashcanon
2018-04-04check-owners.sh: add --show-patterns and --owner optionsGaëtan Gilbert
```bash $ dev/tools/check-owners.sh --show-patterns Makefile Makefile.build /Makefile*: @letouzey $ dev/tools/check-owners.sh --owner '@gares' stm/stm.ml interp/declare.ml stm/stm.ml: @gares $ dev/tools/check-owners.sh --show-patterns --owner '@gares' stm/*.ml interp/*.ml /stm/: @gares ```
2018-04-04Script to identify the code owner for given filesGaëtan Gilbert
Can be used with git diff --name-only to identify owners for changes in given commits.
2018-04-03merge-pr.sh: cache github API callsGaëtan Gilbert
2018-03-31pre-commit: verify user overlay extensions (must be .sh).Gaëtan Gilbert
This has come up a couple times.
2018-03-23improve merge-pr scriptEnrico Tassi
The script now performs many more checks and reports errors in a more intelligible way.
2018-02-24Merge PR #6803: coqdev.el: add space at the end of compile-commandMaxime Dénès
2018-02-21Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Maxime Dénès
2018-02-21coqdev.el: add space at the end of compile-commandGaëtan Gilbert
That way you can just type [-j] instead of having to remember to add a space yourself.
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-13coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGaëtan Gilbert
(and alist-alist)
2018-02-13coqdev.el: fix "compilate"-command typoGaëtan Gilbert
2018-02-13coqdev.el: shell-quote-argument the directory for make -CGaëtan Gilbert
2018-02-13coqdev.el: stop using when-let for emacs<25 compatibility.Gaëtan Gilbert
2018-02-12Merge PR #6565: [Backport script] Check .mli files are not changed.Maxime Dénès
2018-02-11Merge anomaly-traces-parser.el into coqdev.el.Gaëtan Gilbert
2018-02-11coqdev.el: add installation instructions.Gaëtan Gilbert
2018-02-08pre-commit: nicer messagesGaëtan Gilbert
2018-02-08pre-commit: fail gracefully if fixing whitespace removes all changesGaëtan Gilbert
2018-02-08pre-commit: add files after fixing ending newlines.Gaëtan Gilbert
2018-02-08Have the pre-commit hook also fix end-of-file nlJason Gross
2018-02-08Auto-create .git/hooks/pre-commit on ./configureJason Gross
The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files.
2018-02-08pre-commit hook: fix whitespace error detectionGaëtan Gilbert
--quiet implies --exit-code
2018-02-08A pre-commit hook to magically fix whitespace issues.Gaëtan Gilbert
2018-01-23Use travis_retry on apt-get updateJason Gross
Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration.
2018-01-23Merge PR #6568: Cleanup scriptsMaxime Dénès
2018-01-16merge-pr.sh: use git diff --quietGaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
2018-01-10Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelMaxime Dénès
2018-01-09[Backport script] Check .mli files are not changed.Théo Zimmermann
2018-01-08github-check-prs.py: print PR URLs when needed.Gaëtan Gilbert
2018-01-08github-check-prs.py: Strip spaces from token from command lineGaëtan Gilbert
2018-01-08github-check-prs.py: command line option to get token from a fileGaëtan Gilbert
2018-01-06Remove dir-locals and ship suggested helper hooks instead.Gaëtan Gilbert
.dir-locals led to issues with unsafe local variable warnings. With this method the user is opting in to running this code so there are no warnings.
2017-12-30Expound on dependencies for github-check-prs.pyGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 13:07:02 +0000