Juergen Gross, le lun. 17 août 2020 11:49:22 +0200, a ecrit: > diff --git a/stubdom/Makefile b/stubdom/Makefile > index 6fcecadeb9..440adc2eb4 100644 > --- a/stubdom/Makefile > +++ b/stubdom/Makefile
> diff --git a/stubdom/mini-os.mk b/stubdom/mini-os.mk > index 32528bb91f..b1387df3f8 100644 > --- a/stubdom/mini-os.mk > +++ b/stubdom/mini-os.mk For these, Reviewed-by: Samuel Thibault <samuel.thiba...@ens-lyon.org>
