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

Merge pull request #170 from HEPLean/informal_defs

Browse source 
docs: Change graph title
This commit is contained in:
Joseph Tooby-Smith 2024-09-28 13:30:01 +00:00 • committed by GitHub
commit ba38f16ace
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/MetaPrograms/informal.lean
View file

@ -388,7 +388,7 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
<!DOCTYPE html>
<html>
<head>
<title>Interactive Graph with Node-Specific Text Display</title>
<title>Informal dependency graph for HepLean</title>
<style>
/* Optional styling for the message display */
#message {
@ -413,7 +413,7 @@ unsafe def toHTML (imports : Array Import) : MetaM String := do
<script src=\"https://unpkg.com/d3-graphviz@3.0.5/build/d3-graphviz.js\"></script>
<!-- Add a title to the page -->
<h1 style=\"text-align: center;\">Interactive Graph</h1>
<h1 style=\"text-align: center;\">Informal dependency graph for HepLean</h1>
<!-- Div to display the graph -->
<div id=\"graph\" style=\"width: 100vw; height: 75vh; border: 1px solid black\"></div>