Re: [PATCH v3 1/3] stubdom: fix build with disabled pv-grub

[Ian Jackson <iwj@xxxxxxxxxxxxxx>]

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 <jgross@xxxxxxxx>
> Reviewed-by: Samuel Thibault <samuel.thibault@xxxxxxxxxxxx>

Reviewed-by: Ian Jackson <iwj@xxxxxxxxxxxxxx>