diff options
| author | Jessica Clarke | 2020-09-27 16:38:03 +0100 |
|---|---|---|
| committer | Jessica Clarke | 2020-09-27 16:38:03 +0100 |
| commit | 36159bc54164916c555716123c1c63a466952db0 (patch) | |
| tree | 9810a81396e81e504fb9f963378be1394c6d2015 /src/slice.mli | |
| parent | 8065e4bb4a8dcd1eaa4791058bf9581b254b84da (diff) | |
latex: Prepend opt_prefix inside latex_cat_id
Now that the category is prepended in latex_cat_id, also prepend
opt_prefix there instead to ensure no caller forgets to do so.
No functional change intended, and verified by regenerating the LaTeX
for sail-cheri-mips and sail-cheri-riscv.
Diffstat (limited to 'src/slice.mli')
0 files changed, 0 insertions, 0 deletions