idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-05 15:08:00 +03:00
Code Issues Projects Releases Wiki Activity
1,875 Commits 5 Branches 9 Tags 118 MiB
0ab5fe2535
Commit Graph

4 Commits

Author SHA1 Message Date
Johann Rudloff
182a3caa3e [ docs ] Fix strange indentation on WebKit-based browsers (partial fix for #1367) 2021-05-03 11:44:42 +01:00
Johann Rudloff
3dd5878e22 [ wip ] Improve HTML docs with better annotations 2021-04-26 23:02:25 +02:00
Johann Rudloff
ae9da0e8ce Reformat docs CSS file to comply with code style guide (and make the linter happy) 2021-04-26 22:48:24 +02:00
Johann Rudloff
68a5f1f1b7 Copy styles.css from support into generated docs/ folder 2021-04-26 22:45:14 +02:00