Skip to content

Commit

Permalink
Adding an art page (#771)
Browse files Browse the repository at this point in the history
Co-authored-by: Andrej Bauer <andrej.bauer@andrej.com>
Co-authored-by: Matej Petković <Petkomat@users.noreply.github.com>
  • Loading branch information
3 people committed Sep 14, 2023
1 parent adf864e commit 533cff1
Show file tree
Hide file tree
Showing 5 changed files with 14 additions and 1 deletion.
8 changes: 8 additions & 0 deletions ART.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# Agda-unimath art

<div align="center" style="margin: 2em 0;">
<figure>
<img src="agda-unimath-black-and-gold.png" alt="The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023" width="80%">
<figcaption>The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023</figcaption>
</figure>
</div>
4 changes: 3 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ AGDA ?= agda $(AGDAVERBOSE)
TIME ?= time

METAFILES := \
ART.md \
CITE-THIS-LIBRARY.md \
CODINGSTYLE.md \
CONTRIBUTING.md \
Expand Down Expand Up @@ -74,13 +75,14 @@ SUMMARY.md: ${AGDAFILES}
website-prepare: agda-html ./SUMMARY.md
@cp $(METAFILES) ./docs/
@cp ./theme/images/agda-unimath-logo.svg ./docs/
@cp ./theme/images/agda-unimath-black-and-gold.png ./docs/

.PHONY: website
website: website-prepare
@mdbook build

.PHONY: serve-website
serve-website:
serve-website: website-prepare
@mdbook serve -p 8080 --open -d ./book/html

.PHONY: graph
Expand Down
1 change: 1 addition & 0 deletions scripts/generate_main_index_file.py
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ def generate_index(root, header):
- [The library coding style](CODINGSTYLE.md)
- [Guidelines for mixfix operators](MIXFIX-OPERATORS.md)
- [Citing the library](CITE-THIS-LIBRARY.md)
- [Art](ART.md)
{module_index}
"""
Expand Down
Binary file added theme/images/agda-unimath-black-and-gold.png
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 2 additions & 0 deletions theme/js/custom.js
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ if (link) {
// console.log(link);
var filename = link.getAttribute('href');
const fileList = [
'ART.md',
'CITE-THIS-LIBRARY.md',
'CODINGSTYLE.md',
'CONTRIBUTING.md',
Expand All @@ -14,6 +15,7 @@ if (link) {
'HOWTO-INSTALL.md',
'LICENSE.md',
'MAINTAINERS.md',
'MIXFIX-OPERATORS.md',
'README.md',
'STATEMENT-OF-INCLUSION.md',
'SUMMARY.md',
Expand Down

0 comments on commit 533cff1

Please sign in to comment.