diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-11 14:39:19 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-11 14:39:19 +0000 |
| commit | fe0e355164bf8401ee5f2397584d3e3a04b82240 (patch) | |
| tree | 34cf1b61daf7b26ad8cd9c23447e4c5ce07775e3 /install.sh | |
| parent | c3acdf3caca52e3b09ac075f043c4eddfe5d0814 (diff) | |
Gestion des espaces dans les noms + guess_coqlib sous Windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11921 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'install.sh')
| -rwxr-xr-x | install.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/install.sh b/install.sh index 0719ca778..277222f58 100755 --- a/install.sh +++ b/install.sh @@ -1,13 +1,13 @@ #! /bin/sh -dest=$1 +dest="$1" shift for f; do bn=`basename $f` dn=`dirname $f` - install -d $dest/$dn - install -m 644 $f $dest/$dn/$bn + install -d "$dest/$dn" + install -m 644 $f "$dest/$dn/$bn" done |