aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Collapse)Author
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
2017-12-30Python script checking missing/unnecessary [needs: rebase] labelGaëtan Gilbert
2017-12-24Update backport script for more control.Théo Zimmermann
2017-11-29Fix usage comment.Théo Zimmermann
2017-11-29This script apparently uses bash-specific features.Théo Zimmermann
2017-11-29Fix PR merge script.Théo Zimmermann
Was still relying on the existence of user-configured /pr/.
2017-11-28Add PR backport script.Théo Zimmermann
2017-11-28Add PR merge script.Maxime Dénès
2017-11-23Linter: do not lint untracked files.Gaëtan Gilbert
2017-11-20Disable whitespace linter for .out files.Gaëtan Gilbert
2017-10-25Linter: check that files end with newlines.Gaëtan Gilbert
We use git check-attr to look at the same files as git diff --check.
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
They seem unused since 8f4b7f1 (2007).
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-04-04Merge remote-tracking branch 'origin/pr/78' into trunk:Maxime Dénès
An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
2016-03-12Removing an empty file detected by Luc Grateau.Hugo Herbelin
2015-06-26dev/tool/anomaly-traces-parser.elGabriel Scherer
An .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output.
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
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
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13322 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
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
2006-09-29Reactivation des outils de developpement de Jacekherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29Fix broken paths.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8874 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Restructuration dossier dev et mise à jour de certaines documentationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:35:29 +0000