diff options
Diffstat (limited to 'extras/mini-os/Config.mk')
| -rw-r--r-- | extras/mini-os/Config.mk | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/extras/mini-os/Config.mk b/extras/mini-os/Config.mk index 15f7ed832c..96dd739ce7 100644 --- a/extras/mini-os/Config.mk +++ b/extras/mini-os/Config.mk @@ -55,11 +55,3 @@ DEF_CPPFLAGS += -DHAVE_LWIP DEF_CPPFLAGS += -I$(LWIPDIR)/src/include DEF_CPPFLAGS += -I$(LWIPDIR)/src/include/ipv4 endif - -ifneq ($(QEMUDIR),) -qemu=y -endif - -ifneq ($(CAMLDIR),) -caml=y -endif |