aboutsummaryrefslogtreecommitdiffhomepage
path: root/install.sh
Commit message (Expand)AuthorAge
* Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
* Add timing scriptsGravatar Jason Gross2017-07-11
* Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...Gravatar Pierre Boutillier2014-12-17
* Remove bashismsGravatar glondu2010-01-28
* Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchGravatar herbelin2009-04-08
* Gestion des espaces dans les noms + guess_coqlib sous WindowsGravatar notin2009-02-11
* Remplacement de cp --parents par un script shGravatar notin2009-01-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 00:15:07 +0000