You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The mason doc command uses chpldoc to generate docs for the project, storing the html in a /doc directory.
Like the project's binaries in the /target directory, the docs aren't something the user necessary wants to commit to their repo. Should mason automatically add /doc to the project's .gitignore (either when creating the project or generating the docs)?
Note that we already to this for /target.
(alternatively, we could put the /doc directory in /target to avoid this issue)
The text was updated successfully, but these errors were encountered:
I think having mason include the /doc in the .gitignore when creating the project would indeed be very nice. Having mason doc modify and existing .gitignore sounds maybe a bit riskier or at least proner to issues?
The
mason doc
command uses chpldoc to generate docs for the project, storing the html in a/doc
directory.Like the project's binaries in the
/target
directory, the docs aren't something the user necessary wants to commit to their repo. Should mason automatically add/doc
to the project's.gitignore
(either when creating the project or generating the docs)?Note that we already to this for
/target
.(alternatively, we could put the
/doc
directory in/target
to avoid this issue)The text was updated successfully, but these errors were encountered: