Entries are currently added manually to index.md.
The file index.html is generated using
pandoc as follows:
pandoc -f markdown+emoji -s -o index.html index.md-
Notifications
You must be signed in to change notification settings - Fork 0
Rocq-community website
License
rocq-community/rocq-community.github.io
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Rocq-community website