Joshua Potter
cda229ac12
Add nameext to distinguish PDF and HTML files.
2023-12-14 17:09:10 -07:00
96870507c5
feat: add jump-src.js for #src links
2023-09-21 11:38:22 +02:00
924be4c7d8
feat: expand the current file in the navbar
2023-09-18 23:55:19 +02:00
cc552ed570
add colorscheme toggle
2023-06-09 23:39:59 +02:00
033003c6cb
Add a search page to the docs.
...
Now instead of clicking the "Google Site Search"' button, the user has the option
of clicking the "Search" button, which will take them to a results page. Currently,
the results are identical to the autocomplete results, but the number of results
is not limited to 30. In the future, more information and search options could
be added to this page to make a more powerful search.
Fixes #107
2023-01-28 23:00:53 +01:00
3a5c0db46b
style: refactor process to Lean 4 compiler style
2023-01-01 19:30:28 +01:00
72034b0831
feat: linkify builtin types
2022-11-22 21:07:59 +01:00
9aef28b16e
chore: update toolchain 10-20 ( #86 )
2022-10-20 19:51:26 +02:00
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
2cc851aaf1
fix: include top-level modules in hierarchy and exclude non-html
2022-07-23 22:02:20 -04:00
ed4cee2eae
chore: style, change $ to <|
2022-07-23 13:01:25 +02:00
c29cf7b70c
feat: index shall not depend on importing things
2022-07-22 00:34:13 +02:00
25b1ddb66b
feat: Preparations to split doc-gen build process
2022-07-21 01:40:04 +02:00
279df92555
refactor: restructure the modules
2022-05-19 20:41:07 +02:00
Joshua Potter
Mario Carneiro
Alex J. Best
Calvin Lee
Jeremy Salwen
Henrik Böving
tydeu