diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-22 12:53:53 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-22 12:53:53 +0000 |
| commit | bd1e95c45668aedb39e70d1aae90a9bb86534506 (patch) | |
| tree | 04bbe2cf3b97d2c7b2fac582eb3380b2ec0f2c30 /configure | |
| parent | 311572e0c1375429de998d70eb7d587d7b8032c4 (diff) | |
Using .local instead of ./.local in READMEs
Until now, in the instructions, we were suggesting to run
`./.local/bin/make', but the `./' part is extra: this is already a
directory and so the shell will be able to find it. So to make things more
clear and easy to read/write, we removed the `./' part from the calls to
our custom Make installation.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -570,7 +570,7 @@ The reproduction pipeline and its environment are configured with no errors. Please run the following command to start. (Replace '8' with the number of CPU threads) - ./.local/bin/make -j8 + .local/bin/make -j8 To change the configuration later, please re-run './configure', DO NOT manually edit the relevant files. |