aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Expand)Author
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 17:00:52 +0000