Merge remote-tracking branch 'origin/master' into feature/patrick/merge-master-in-dune
TESTS NOT MERGED
No related branches found
No related tags found
Showing
- .Makefile.lint 0 additions, 39 deletions.Makefile.lint
- .git-blame-ignore-revs 25 additions, 0 deletions.git-blame-ignore-revs
- .gitignore 7 additions, 3 deletions.gitignore
- .gitlab-ci.yml 12 additions, 0 deletions.gitlab-ci.yml
- .gitlab/issue_templates/bug_report.md 2 additions, 1 deletion.gitlab/issue_templates/bug_report.md
- ALL_VERSIONS 1 addition, 0 deletionsALL_VERSIONS
- Changelog 32 additions, 0 deletionsChangelog
- INSTALL.md 7 additions, 8 deletionsINSTALL.md
- LICENSE 8 additions, 0 deletionsLICENSE
- Makefile.generating 19 additions, 19 deletionsMakefile.generating
- README.md 5 additions, 4 deletionsREADME.md
- VERSION 1 addition, 1 deletionVERSION
- VERSION_CODENAME 1 addition, 1 deletionVERSION_CODENAME
- bin/build-src-distrib.sh 720 additions, 248 deletionsbin/build-src-distrib.sh
- bin/check-reference-configuration.sh 1 addition, 1 deletionbin/check-reference-configuration.sh
- bin/check_newline.sh 37 additions, 0 deletionsbin/check_newline.sh
- bin/frama-c-config 1 addition, 4 deletionsbin/frama-c-config
- bin/frama-c.debug 0 additions, 1 deletionbin/frama-c.debug
- bin/migration_scripts/titanium2vanadium.sh 184 additions, 0 deletionsbin/migration_scripts/titanium2vanadium.sh
- bin/update_api_doc.sh 1 addition, 1 deletionbin/update_api_doc.sh
Loading
Please register or sign in to comment