aboutsummaryrefslogtreecommitdiff
path: root/install.sh
AgeCommit message (Expand)Author
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2017-07-11Add timing scriptsJason Gross
2014-12-17Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...Pierre Boutillier
2010-01-28Remove bashismsglondu
2009-04-08Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchherbelin
2009-02-11Gestion des espaces dans les noms + guess_coqlib sous Windowsnotin
2009-01-22Remplacement de cp --parents par un script shnotin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:03:12 +0000