git status, I see
# Untracked files: # coq-core.install # coqide-server.install # coqide.install
Should these be added to
.gitgnore? (Should it be
*.install? A specific list?)
@Jason Gross newer dune versions put these files under
_build, hence for most devs the .gitignore is not needed anymore.
Last updated: Nov 29 2023 at 21:01 UTC