diff --git a/config/Stubdom.mk.in b/config/Stubdom.mk.in index 5990fc4e04..b399d77740 100644 --- a/config/Stubdom.mk.in +++ b/config/Stubdom.mk.in @@ -26,9 +26,6 @@ LWIP_URL := @LWIP_URL@ GRUB_VERSION := @GRUB_VERSION@ GRUB_URL := @GRUB_URL@ -OCAML_VERSION := @OCAML_VERSION@ -OCAML_URL := @OCAML_URL@ - GMP_VERSION := @GMP_VERSION@ GMP_URL := @GMP_URL@