Juergen Gross writes ("[PATCH v3 1/3] stubdom: fix build with disabled
pv-grub"):
> Today the build will fail if --disable-pv-grub as a parameter of
> configure, as the main Makefile will unconditionally try to build a
> 32-bit pv-grub stubdom.
>
> Fix that by introducing a pv-grub-if-enabled target in
> stubdom/Makefile taking care of this situation.
>
> Signed-off-by: Juergen Gross <[email protected]>
> Reviewed-by: Samuel Thibault <[email protected]>
Reviewed-by: Ian Jackson <[email protected]>
