Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a siteinfo JSON file generated by makedocs #2181

Merged
merged 4 commits into from Jul 14, 2023
Merged

Add a siteinfo JSON file generated by makedocs #2181

merged 4 commits into from Jul 14, 2023

Conversation

mortenpi
Copy link
Member

@mortenpi mortenpi commented Jul 12, 2023

A sibling to the siteinfo.js file generated by deploydocs. The point here is that this one will always be generated, but will not actually be read by the HTML. Instead, this can be used by external tools, like DocumenterTools, to figure out what version of Documenter was used to generate the docs etc.

We could try to re-use siteinfo.js for this new metadata as well, but it is convenient if the metadata is in a standard, structured format that can easily be parsed. siteinfo.js must be valid top-level JS, and therefore would need a custom parser.

@mortenpi mortenpi added Type: Enhancement Format: HTML Related to the default HTML output labels Jul 12, 2023
@mortenpi mortenpi enabled auto-merge (squash) July 14, 2023 01:13
@mortenpi mortenpi merged commit 4643dbf into master Jul 14, 2023
20 of 21 checks passed
@mortenpi mortenpi deleted the mp/siteinfo branch July 14, 2023 01:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Format: HTML Related to the default HTML output Type: Enhancement
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant