Vladimír Čunát 8adabe6679 gawk: split $doc into $man and $info ... Info files are rather large and not much used anymore, AFAIK. (We include $man or $doc in the system closure by default.)		2015-10-28 10:16:55 +01:00
..
default.nix	gawk: split $doc into $man and $info	2015-10-28 10:16:55 +01:00