Stream: Coq devs & plugin devs

Topic: Untracked files

view this post on Zulip Jason Gross (Jul 28 2023 at 00:25):

With git status, I see

# Untracked files:
#       coq-core.install
#       coqide-server.install
#       coqide.install

Should these be added to .gitgnore? (Should it be ./*.install? *.install? A specific list?)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 15:23):

@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