Release script
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
Loading
Please register or sign in to comment