-
Georges Racinet authored
This looks somewhat redundant, but `make` is not currently available in the CI image. We could add it (but not the whole toolchain) but it's not worth the effort for now.
045bc68c6edc
This looks somewhat redundant, but `make` is not currently available in the CI image. We could add it (but not the whole toolchain) but it's not worth the effort for now.