diff options
| author |  lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 15:13:04 +0000 |
|---|---|---|
| committer | lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 15:13:04 +0000 |
| commit | f0127d555ca0143323854c48587e3b05fb370f9d (patch) | |
| tree | 94484f05f8c3609616f85e5a0d48038ad5416d51 /INSTALL | |
| parent | 2f088e269c88978e89f43f6b3c01021e782735eb (diff) | |
Oups... Use shell-variable syntax in shell commands.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10023 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -53,10 +53,10 @@ WHAT DO YOU NEED ? bzip9 -cd make-3.81.tar.bz2 | tar x #If you don't have bzip2, you can download the gzipped version instead. cd make-3.81 - ./configure --prefix=$(HOME) + ./configure --prefix=${HOME} make install - Then, make sure that $(HOME)/bin is first in your $PATH. + Then, make sure that ${HOME}/bin is first in your $PATH. ) - a C compiler |