diff options
| author | Alasdair Armstrong | 2020-09-28 14:22:25 +0100 |
|---|---|---|
| committer | GitHub | 2020-09-28 14:22:25 +0100 |
| commit | c79b2759fa85373d25c1d2d64c3599a5773a4c68 (patch) | |
| tree | 5785eae9917e860ab8f5168bcee4f4c872c81256 /src/slice.mli | |
| parent | 882850db49cffef75e11eef8cf00364611e54e19 (diff) | |
| parent | 57fd06728f923d039c3f60d116f646c136528b77 (diff) | |
Merge pull request #97 from jrtc27/label-prefix
latex: Prefix label names with the specified -latex_prefix
Diffstat (limited to 'src/slice.mli')
0 files changed, 0 insertions, 0 deletions