aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Expand)Author
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
2018-02-08pre-commit hook: fix whitespace error detectionGaëtan Gilbert
2018-02-08A pre-commit hook to magically fix whitespace issues.Gaëtan Gilbert
2018-01-23Use travis_retry on apt-get updateJason Gross
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
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
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
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
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
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
2016-03-12Removing an empty file detected by Luc Grateau.Hugo Herbelin
2015-06-26dev/tool/anomaly-traces-parser.elGabriel Scherer
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2006-09-29Reactivation des outils de developpement de Jacekherbelin
2006-05-29Fix broken paths.msozeau
2006-05-23Restructuration dossier dev et mise à jour de certaines documentationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:22:03 +0000