aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Collapse)AuthorAge
* 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.
| * | Expound on dependencies for github-check-prs.pyGravatar Gaëtan Gilbert2017-12-30
| | |
| * | Python script checking missing/unnecessary [needs: rebase] labelGravatar Gaëtan Gilbert2017-12-30
| |/
* / Update backport script for more control.Gravatar Théo Zimmermann2017-12-24
|/
* Fix usage comment.Gravatar Théo Zimmermann2017-11-29
|
* This script apparently uses bash-specific features.Gravatar Théo Zimmermann2017-11-29
|
* Fix PR merge script.Gravatar Théo Zimmermann2017-11-29
| | | | Was still relying on the existence of user-configured /pr/.
* Add PR backport script.Gravatar Théo Zimmermann2017-11-28
|
* Add PR merge script.Gravatar Maxime Dénès2017-11-28
|
* Linter: do not lint untracked files.Gravatar Gaëtan Gilbert2017-11-23
|
* Disable whitespace linter for .out files.Gravatar Gaëtan Gilbert2017-11-20
|
* Linter: check that files end with newlines.Gravatar Gaëtan Gilbert2017-10-25
| | | | We use git check-attr to look at the same files as git diff --check.
* Remove unused Makefiles in dev/tools/Gravatar Gaëtan Gilbert2017-08-01
| | | | They seem unused since 8f4b7f1 (2007).
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* Merge remote-tracking branch 'origin/pr/78' into trunk:Gravatar Maxime Dénès2016-04-04
|\ | | | | | | | | An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
* | Removing an empty file detected by Luc Grateau.Gravatar Hugo Herbelin2016-03-12
| |
| * dev/tool/anomaly-traces-parser.elGravatar Gabriel Scherer2015-06-26
|/ | | | | An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
| | | | | | | By the way, definitely remove "Dump Universes", which has been deprecated since 2006 (r9306). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13754 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated COPYRIGHT file and header. Improved and fixed header updater.Gravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13322 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reactivation des outils de developpement de JacekGravatar herbelin2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix broken paths.Gravatar msozeau2006-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8874 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:26:02 +0000