diff options
| author | Marcello Stanisci <marcello.stanisci@inria.fr> | 2017-10-17 13:06:13 +0200 |
|---|---|---|
| committer | Marcello Stanisci <marcello.stanisci@inria.fr> | 2017-10-17 13:06:13 +0200 |
| commit | 40c0d0cf545ce2b2390a3f0e51b23eb848a4c2f4 (patch) | |
| tree | 0f37353ccc7e5626692ced0cc3da2ead53c9ada3 /README | |
| parent | dba82cb7f98575338037aeee4d72620d2e5a7d9e (diff) | |
| download | bank-40c0d0cf545ce2b2390a3f0e51b23eb848a4c2f4.tar.gz bank-40c0d0cf545ce2b2390a3f0e51b23eb848a4c2f4.tar.bz2 bank-40c0d0cf545ce2b2390a3f0e51b23eb848a4c2f4.zip | |
README
Diffstat (limited to 'README')
| -rw-r--r-- | README | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -31,6 +31,9 @@ The next step is to specify the install prefix, run $ export PREFIX=$HOME/local # Adapt to your needs. $ ./configure --prefix=$PREFIX +On some Debian systems, the additional flag --enable-debian-system +might be useful to let the --prefix option be correctly executed. + Then the usual GNU-compatible commands, that are $ make install |