Merge branch 'cj-release' into 'master'
Release script See merge request !45
Showing
- .gitlab-ci.yml 53 additions, 2 deletions.gitlab-ci.yml
- CHANGES.md 8 additions, 0 deletionsCHANGES.md
- Makefile 48 additions, 8 deletionsMakefile
- changelog.sed 44 additions, 0 deletionschangelog.sed
- tools/.gitignore 1 addition, 0 deletionstools/.gitignore
- tools/Makefile 2 additions, 0 deletionstools/Makefile
- tools/colibri_for_bundle.ml 0 additions, 0 deletionstools/colibri_for_bundle.ml
- tools/colibri_for_bundle.opam 27 additions, 0 deletionstools/colibri_for_bundle.opam
- tools/compile_colibri.ml 1 addition, 1 deletiontools/compile_colibri.ml
- tools/compile_colibri.opam 27 additions, 0 deletionstools/compile_colibri.opam
- tools/dune 20 additions, 0 deletionstools/dune
- tools/dune-project 25 additions, 0 deletionstools/dune-project
CHANGES.md
0 → 100644
changelog.sed
0 → 100644
tools/.gitignore
0 → 100644
tools/Makefile
0 → 100644
File moved
tools/colibri_for_bundle.opam
0 → 100644
tools/compile_colibri.opam
0 → 100644
tools/dune
0 → 100644
tools/dune-project
0 → 100644
Please register or sign in to comment