Closed ronaldtse closed 2 years ago
Should we change this repo to just "scripts" instead of "metanorma-build-scripts"?
Feels a bit redundant with such a long name. This repository won't be used by others outside the project.
As agreed with @CAMOBAP , it will be "ci".
Done.
Should we change this repo to just "scripts" instead of "metanorma-build-scripts"?
Feels a bit redundant with such a long name. This repository won't be used by others outside the project.