noweb: remove noweb_awk

This commit is contained in:
Eric Bailey 2019-08-13 13:06:01 +02:00
parent 3f2ba625d6
commit 6db22bca4b

View File

@ -9684,9 +9684,9 @@ in
gconf = pkgs.gnome2.GConf;
};
noweb = noweb_icon;
noweb_awk = noweb_icon.override { icon-lang = null; };
noweb_icon = callPackage ../development/tools/literate-programming/noweb { };
# NOTE: Override and set icon-lang = null to use Awk instead of Icon.
noweb = callPackage ../development/tools/literate-programming/noweb { };
nuweb = callPackage ../development/tools/literate-programming/nuweb { tex = texlive.combined.scheme-small; };
nrfutil = callPackage ../development/tools/misc/nrfutil { };