summarylogtreecommitdiffstats
path: root/.gitignore
AgeCommit message (Expand)Author
2023-04-30Do not opam init if $HOME/.opam/config already existsThomas Letan