Repository navigation
'make install' ignores --prefix for installing the man page #2984
Description
Hi,
Using today’s master from git, I’m running:
./configure --prefix /home/simon/non-packages
make # fails for some reason
make # succeeds
make install # without sudo
make fails the first time with this output: http://nopaste.info/d3df650be4.html , but finishes without error the second time. I’m told on IRC that that issue is already reported (edit: #2641).
This issue is with make install. It ignores the prefix and tries (and fails, since I’m not root) to create /usr/local/share/man/man1. It should write to /home/simon/non-packages/share/man/man1 instead.
Activity
SimonSapin commentedon Jul 21, 2012
I tried to trick Make with a symlink, but now it tries to write to
/usr/local/bin/rustc. It appear to ignore the prefix completely.SimonSapin commentedon Jul 21, 2012
It worked with
--prefix=foo(which is indeed how it appears in the --help message) instead of--prefix foo. My fault for not reading carefully enough, although it would be nice to have both work.nikomatsakis commentedon Jul 23, 2012
Seems like the bug has more to do with command-line parsing than installation. Closing the issue.
nikomatsakis commentedon Jul 23, 2012
I was going to open a bug for support
--prefix arg, except that near as I can tell--prefix=argis the standard form and--prefix argis not normally accepted in other configure scripts.Auto merge of rust-lang#2984 - RalfJung:soundness, r=RalfJung
Bump Kani version to 0.45.0 (rust-lang#2984)
Merge pull request rust-lang#2984 from rust-lang/bump-check-version