Skip to content

Commit

Permalink
Fix style
Browse files Browse the repository at this point in the history
  • Loading branch information
Ailrun committed Sep 27, 2024
1 parent 1895405 commit 091598d
Show file tree
Hide file tree
Showing 5 changed files with 3 additions and 7 deletions.
2 changes: 1 addition & 1 deletion assets/extra/header.html
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="resources/config.js"></script>
<script type="text/javascript" src="resources/coqdocjs.js"></script>
</head>
Expand Down
1 change: 0 additions & 1 deletion assets/extra/resources/coqdocjs.css
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,6 @@ html, body {
padding-bottom: 2em;
margin-left: auto;
margin-right: auto;
max-width: 60em;
flex: 1 0 auto;
}

Expand Down
4 changes: 0 additions & 4 deletions assets/extra/resources/depgraph.css
Original file line number Diff line number Diff line change
@@ -1,7 +1,3 @@
div.#main {
max-width: unset;
}

svg.depgraph {
max-width: 100%;
}
Expand Down
1 change: 1 addition & 0 deletions assets/extra/resources/depgraph.js
Original file line number Diff line number Diff line change
Expand Up @@ -44,3 +44,4 @@ function makeEdgesInteractive(evt) {
polygon.style.opacity = '1';
}, 1000 * timeUnit);
}
}
2 changes: 1 addition & 1 deletion scripts/post_process_dep.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
SVG_ELEMENT.setAttribute("onload", "makeEdgesInteractive(evt)")
for line in io.open(PROJECT_ROOT / "assets" / "extra" / "header.html"):
print(line, end='')
print('<link href="resources/depgraph.css" rel="stylesheet" type="text/css"/>')
print('<link href="resources/depgraph.css" rel="stylesheet" type="text/css" />')
print('<script type="text/javascript" src="resources/depgraph.js"></script>')
SVG_ELEMENT.writexml(sys.stdout)
for line in io.open(PROJECT_ROOT / "assets" / "extra" / "footer.html"):
Expand Down

0 comments on commit 091598d

Please sign in to comment.