Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add new options --no-conflict and --no-signature-check to backport script. | Théo Zimmermann | 2018-07-10 |
| | |||
* | [merge script] Check if the CI that was run is outdated. | Théo Zimmermann | 2018-06-09 |
| | | | | [ci skip] | ||
* | [doc] Add an ELisp snippet to insert Sphinx roles and quotes | Clément Pit-Claudel | 2018-05-15 |
| | |||
* | Merge PR #7170: Script to identify the code owner for given files | Maxime Dénès | 2018-05-14 |
|\ | |||
* \ | Merge PR #7337: dir-locals: add bug-reference-mode variables | Emilio Jesus Gallego Arias | 2018-05-14 |
|\ \ | |||
| * | | coqdev.el: add bug-reference-mode variables | Gaëtan Gilbert | 2018-05-11 |
| | | | |||
* | | | use at least 6 Xs in mktemp filename templates | Sven M. Hallberg | 2018-05-09 |
|/ / | | | | | | | OpenBSD mktemp fails with an error otherwise. | ||
| * | Add check-owners-pr.sh wrapper around check-owners | Gaëtan Gilbert | 2018-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 doc | Maxime Dénès | 2018-04-19 |
|\ \ | |||
* | | | pre-commit : do not fail miserably if git config has `apply.whitespace = fix` | Pierre Letouzey | 2018-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 doc | Pierre Courtieu | 2018-04-11 |
|/ / | |||
* | | Merge script: adds a way for confirmation to expect a newline. | Théo Zimmermann | 2018-04-09 |
| | | | | | | | | This fulfils Gaetan's wish. | ||
* | | Add sanity check in merge script: local branch is up-to-date. | Théo Zimmermann | 2018-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. | Théo Zimmermann | 2018-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. | Théo Zimmermann | 2018-04-08 |
| | | | | | | | | This should solve Emilio's problem. | ||
* | | Merge script: use fetch URL for the remote. | Théo Zimmermann | 2018-04-08 |
| | | | | | | | | In case the push URL has been overriden to make it fetch-only. | ||
* | | Improve shell scripts | zapashcanon | 2018-04-05 |
| | | |||
| * | check-owners.sh: add --show-patterns and --owner options | Gaëtan Gilbert | 2018-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 files | Gaëtan Gilbert | 2018-04-04 |
| | | | | | | | | | | Can be used with git diff --name-only to identify owners for changes in given commits. | ||
* | | merge-pr.sh: cache github API calls | Gaëtan Gilbert | 2018-04-03 |
|/ | |||
* | pre-commit: verify user overlay extensions (must be .sh). | Gaëtan Gilbert | 2018-03-31 |
| | | | | This has come up a couple times. | ||
* | improve merge-pr script | Enrico Tassi | 2018-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-command | Maxime Dénès | 2018-02-24 |
|\ | |||
* \ | Merge PR #6283: A pre-commit hook to magically fix whitespace issues. | Maxime Dénès | 2018-02-21 |
|\ \ | |||
| | * | coqdev.el: add space at the end of compile-command | Gaëtan Gilbert | 2018-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. | Maxime Dénès | 2018-02-19 |
|\ \ | |||
| * | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | Gaëtan Gilbert | 2018-02-13 |
| | | | | | | | | | | | | (and alist-alist) | ||
| * | | coqdev.el: fix "compilate"-command typo | Gaëtan Gilbert | 2018-02-13 |
| | | | |||
| * | | coqdev.el: shell-quote-argument the directory for make -C | Gaëtan Gilbert | 2018-02-13 |
| | | | |||
| * | | coqdev.el: stop using when-let for emacs<25 compatibility. | Gaëtan Gilbert | 2018-02-13 |
| | | | |||
* | | | Merge PR #6565: [Backport script] Check .mli files are not changed. | Maxime Dénès | 2018-02-12 |
|\ \ \ | |||
| | * | | Merge anomaly-traces-parser.el into coqdev.el. | Gaëtan Gilbert | 2018-02-11 |
| | | | | |||
| | * | | coqdev.el: add installation instructions. | Gaëtan Gilbert | 2018-02-11 |
| | | | | |||
| | | * | pre-commit: nicer messages | Gaëtan Gilbert | 2018-02-08 |
| | | | | |||
| | | * | pre-commit: fail gracefully if fixing whitespace removes all changes | Gaëtan Gilbert | 2018-02-08 |
| | | | | |||
| | | * | pre-commit: add files after fixing ending newlines. | Gaëtan Gilbert | 2018-02-08 |
| | | | | |||
| | | * | Have the pre-commit hook also fix end-of-file nl | Jason Gross | 2018-02-08 |
| | | | | |||
| | | * | Auto-create .git/hooks/pre-commit on ./configure | Jason Gross | 2018-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 detection | Gaëtan Gilbert | 2018-02-08 |
| | | | | | | | | | | | | | | | | --quiet implies --exit-code | ||
| | | * | A pre-commit hook to magically fix whitespace issues. | Gaëtan Gilbert | 2018-02-08 |
| | | | | |||
* | | | | Use travis_retry on apt-get update | Jason Gross | 2018-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 scripts | Maxime Dénès | 2018-01-23 |
|\ \ \ | |||
| * | | | merge-pr.sh: use git diff --quiet | Gaëtan Gilbert | 2018-01-16 |
| | | | | |||
| * | | | Cleanup shell expansions and quoting. | Gaëtan Gilbert | 2018-01-16 |
| | | | | |||
| * | | | Simplify logic and streamline lint-repository.sh | Gaëtan Gilbert | 2018-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] label | Maxime Dénès | 2018-01-10 |
|\ \ \ \ | |||
| | | * | | [Backport script] Check .mli files are not changed. | Théo Zimmermann | 2018-01-09 |
| |_|/ / |/| | | | |||
| * | | | github-check-prs.py: print PR URLs when needed. | Gaëtan Gilbert | 2018-01-08 |
| | | | | |||
| * | | | github-check-prs.py: Strip spaces from token from command line | Gaëtan Gilbert | 2018-01-08 |
| | | | | |||
| * | | | github-check-prs.py: command line option to get token from a file | Gaëtan Gilbert | 2018-01-08 |
| | | | |