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

Merge pull request #164 from HEPLean/informal_defs

Browse source 
docs: Change default tooltip for dot graph
This commit is contained in:
Joseph Tooby-Smith 2024-09-20 06:43:16 -04:00 • committed by GitHub
commit 4dc1e6bd9f
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

@ -274,6 +274,7 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do
pack=true;
packmode=\"array1\";
];
tooltip = \"Informal HepLean graph\";
node [margin=0.05; fontsize=10; fontname=\"Georgia\", height=0.1];
bgcolor=\"white\";
label=\"Informal dependency graph for HepLean.