-
Emmanuel Duchastenier authored
that suits the docker version, as it is different from the distrib one. For now, the version is copied, and any modification in the file must be copied to the docker version. With the proposed change, the docker version is generated from the distrib version, with minor changes
42a25600