aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Collapse)AuthorAge
* [merge script] Check if the CI that was run is outdated.Gravatar Théo Zimmermann2018-06-09
| | | | [ci skip]
* [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
|/ / | | | | | | OpenBSD mktemp fails with an error otherwise.
| * Add check-owners-pr.sh wrapper around check-ownersGravatar Gaëtan Gilbert2018-04-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | ``` $ 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 ```
* | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | 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
| | | | | | | | This fulfils Gaetan's wish.
* | Add sanity check in merge script: local branch is up-to-date.Gravatar Théo Zimmermann2018-04-09
| | | | | | | | | | | | 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.
* | Document requirement to have git >= 2.7 to use the merge script.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
* | Merge script does not warn when the remote is set to HTTPS.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | This should solve Emilio's problem.
* | Merge script: use fetch URL for the remote.Gravatar Théo Zimmermann2018-04-08
| | | | | | | | In case the push URL has been overriden to make it fetch-only.
* | Improve shell scriptsGravatar zapashcanon2018-04-05
| |
| * check-owners.sh: add --show-patterns and --owner optionsGravatar Gaëtan Gilbert2018-04-04
| | | | | | | | | | | | | | | | | | | | | | | | | | ```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 ```
| * Script to identify the code owner for given filesGravatar Gaëtan Gilbert2018-04-04
| | | | | | | | | | Can be used with git diff --name-only to identify owners for changes in given commits.
* | 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
| | | | This has come up a couple times.
* improve merge-pr scriptGravatar Enrico Tassi2018-03-23
| | | | | The script now performs many more checks and reports errors in a more intelligible way.
* 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
| |/ |/| | | | | | | That way you can just type [-j] instead of having to remember to add a space yourself.
* | 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
| | | | | | | | | | | | (and alist-alist)
| * | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * pre-commit hook: fix whitespace error detectionGravatar Gaëtan Gilbert2018-02-08
| | | | | | | | | | | | | | | | --quiet implies --exit-code
| | | * 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
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | 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
| | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* | | | 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
| | |/ | | | | | | | | | | | | .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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 21:02:09 +0000