DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #228 from HEPLean/IndexNotation

Browse source 
doc: Add note to informal graph maker
This commit is contained in:
Joseph Tooby-Smith 2024-11-07 08:10:16 +00:00 • committed by GitHub
commit e9980d7076
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/MetaPrograms/informal.lean
View file

@ -16,6 +16,7 @@ import ImportGraph.RequiredModules
To make the dot file for the dependency graph run:
- lake exe informal mkDot
- dot -Tsvg -o ./Docs/graph.svg ./Docs/InformalDot.dot
- or dot -Tpng -Gdpi=300 -o ./Docs/graph.png ./Docs/InformalDot.dot
-/
open Lean System Meta