diff options
| author | nbehrnd <nbehrnd@users.noreply.github.com> | 2024-05-17 15:36:55 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-05-17 07:36:55 -0600 |
| commit | 89857f5e24eda256f978dc44df04ffa729f69273 (patch) | |
| tree | 8559f0672ecf271243eb5b409de41517f08f2b28 /lean4.html.markdown | |
| parent | 21c588354c88b309408b81e738efc6829c9b9c5b (diff) | |
[rst/de] light extension of export formats docutils offers (#4654)
Diffstat (limited to 'lean4.html.markdown')
0 files changed, 0 insertions, 0 deletions