Skip to content

Conversation

@vreuter
Copy link

@vreuter vreuter commented Nov 25, 2025

This combines the redundant sections of the contributing doc, regarding how to build the documentation and serve it locally with Hoogle. This would close #1777 .

Copy link
Member

@dnadales dnadales left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not all of the instructions were properly preserved.

@vreuter
Copy link
Author

vreuter commented Nov 26, 2025

Not all of the instructions were properly preserved.

@dnadales can you clarify what's improperly preserved? In the diff, the pieces of information I see missing in the new version concern

  • running the documentation script
  • the local host address and port number

But those pieces of information are still in the document, and under the same heading.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Duplicated section in document about contributing

2 participants