rename the Makefile.version so that the build works in a fresh docker
Showing
- Makefile 2 additions, 2 deletionsMakefile
- Makefile.dev 0 additions, 10 deletionsMakefile.dev
- Makefile.version.hide 0 additions, 0 deletionsMakefile.version.hide
- README.md 7 additions, 6 deletionsREADME.md
- README.org 1 addition, 0 deletionsREADME.org
- _oasis 1 addition, 1 deletion_oasis
- doc/version.tex 2 additions, 2 deletionsdoc/version.tex
- setup.ml 7269 additions, 0 deletionssetup.ml
- src/META 2 additions, 2 deletionssrc/META
- src/lutilsVersion.ml 2 additions, 2 deletionssrc/lutilsVersion.ml
Loading
Please register or sign in to comment