diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2021-08-05 15:13:07 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-05 15:13:07 +0200 |
| commit | d64f9671fcce47e792974b372dc72de8c49994b7 (patch) | |
| tree | 5ff35626e9472c07027bed709ffe8a49af397f15 /src | |
| parent | 47e96bb533f8cacc171bec9b688b134de31a48a9 (diff) | |
| parent | de39cfb9f39603c61092f01482cb105349187fc6 (diff) | |
Merge pull request #5094 from Pamplemousse/simpler_doc
doc/manual: don't need to copy `highlight.js` manually
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions