bash 4.4: split headers into .dev
This commit is contained in:
parent
40a6918af3
commit
f37566d396
|
@ -25,7 +25,7 @@ stdenv.mkDerivation rec {
|
||||||
|
|
||||||
hardeningDisable = [ "format" ];
|
hardeningDisable = [ "format" ];
|
||||||
|
|
||||||
outputs = [ "out" "doc" "info" ];
|
outputs = [ "out" "dev" "doc" "info" ];
|
||||||
|
|
||||||
# the man pages are small and useful enough
|
# the man pages are small and useful enough
|
||||||
outputMan = if interactive then "out" else null;
|
outputMan = if interactive then "out" else null;
|
||||||
|
@ -79,6 +79,7 @@ stdenv.mkDerivation rec {
|
||||||
|
|
||||||
postInstall = ''
|
postInstall = ''
|
||||||
ln -s bash "$out/bin/sh"
|
ln -s bash "$out/bin/sh"
|
||||||
|
moveToOutput lib/bash/Makefile.inc "$dev"
|
||||||
'';
|
'';
|
||||||
|
|
||||||
postFixup = if interactive
|
postFixup = if interactive
|
||||||
|
|
Loading…
Reference in New Issue