aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
Commit message (Expand)AuthorAge
* 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