aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Expand)AuthorAge
* 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
* 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
* Remove unused Makefiles in dev/tools/Gravatar Gaëtan Gilbert2017-08-01
* 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
|\
* | Removing an empty file detected by Luc Grateau.Gravatar Hugo Herbelin2016-03-12
| * dev/tool/anomaly-traces-parser.elGravatar Gabriel Scherer2015-06-26
|/
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Updated COPYRIGHT file and header. Improved and fixed header updater.Gravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Reactivation des outils de developpement de JacekGravatar herbelin2006-09-29
* Fix broken paths.Gravatar msozeau2006-05-29
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 05:12:15 +0000