swh:1:snp:505c374fd75bb208ae4e9a54e64bb310bc49295e
Raw File
Tip revision: eb86eda63dfe730bac3d9b74c9b4300904a0ca2e authored by Arvid Jakobsson on 26 January 2024, 14:00:45 UTC
CI: Generate [before_merging] pipeline
Tip revision: eb86eda
.gitattributes
_coverage_output export-ignore
.gitignore export-ignore
.gitattributes export-ignore
.gitlab-ci.yml export-ignore
.github export-ignore
.gitlab export-ignore
devtools export-ignore
# these folders have symlinks which are problematic on Windows
docs/active export-ignore

src/lib_version/exe/get_git_info.ml export-subst
src/lib_version/current_git_info.ml export-subst
back to top