From 98b9a2435772388269ee07b78284d833dcf01ccd Mon Sep 17 00:00:00 2001 From: Christian Helmuth Date: Mon, 11 Apr 2016 12:25:56 +0200 Subject: [PATCH] builddir: genode world in optional repositories --- tool/builddir/etc/build.conf.optional | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tool/builddir/etc/build.conf.optional b/tool/builddir/etc/build.conf.optional index 3664c2fa00..0d2c551746 100644 --- a/tool/builddir/etc/build.conf.optional +++ b/tool/builddir/etc/build.conf.optional @@ -34,3 +34,11 @@ # The 'gems' repository depends on 'libc' and 'libports'. # #REPOSITORIES += $(GENODE_DIR)/repos/gems + +# +# Genode world repository +# +# Collection of community-maintained components available at +# https://github.com/genodelabs/genode-world.git +# +#REPOSITORIES += $(GENODE_DIR)/repos/world