aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Collapse)Author
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-16Only check overlay extensions on git-tracked filesJason Gross
This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git.
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
2018-07-10Add new options --no-conflict and --no-signature-check to backport script.Théo Zimmermann
2018-06-09[merge script] Check if the CI that was run is outdated.Théo Zimmermann
[ci skip]
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:32:24 +0000