aboutsummaryrefslogtreecommitdiff
path: root/install.sh
AgeCommit message (Expand)Author
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