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

Node link is hardcoded to mathlib in generated html #61

Open
SnO2WMaN opened this issue Mar 8, 2025 · 0 comments
Open

Node link is hardcoded to mathlib in generated html #61

SnO2WMaN opened this issue Mar 8, 2025 · 0 comments
Labels
enhancement New feature or request

Comments

@SnO2WMaN
Copy link

SnO2WMaN commented Mar 8, 2025

I generated import-graph visualization and deployed to https://formalizedformallogic.github.io/Foundation/book/assets/import_graph.html, but link in node is hardcoded to mathlib's doc.

I know it works when add queryparam e.g. https://formalizedformallogic.github.io/Foundation/book/assets/import_graph.html?docs_url=https://formalizedformallogic.github.io/Foundation/doc/, but it might be good to be able to pass the parameter as url when generating by CLI like lake exe html --doc https://formalizedformallogic.github.io/Foundation/doc.

@joneugster joneugster added the enhancement New feature or request label Mar 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants