diff options
| author | Vincent Laporte | 2020-02-12 07:40:58 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-02-12 10:42:53 +0100 |
| commit | bfa812b40138469ebe5bc3e306da79aa6b050e48 (patch) | |
| tree | bd88296dc97c95b8a303efd2f9fe7c12883ba48d /plugins/syntax/string_notation.ml | |
| parent | 2a4d9569570584c300fcb19c3804fe07578eef12 (diff) | |
[nix] Fix building of the documentation
The interpreter directive of “doc/stdlib/make-library-index” must be patched.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions