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