diff options
| author | Jessica Clarke | 2020-09-27 16:53:48 +0100 |
|---|---|---|
| committer | Jessica Clarke | 2020-09-27 16:53:48 +0100 |
| commit | 57fd06728f923d039c3f60d116f646c136528b77 (patch) | |
| tree | 5785eae9917e860ab8f5168bcee4f4c872c81256 /test | |
| parent | 36159bc54164916c555716123c1c63a466952db0 (diff) | |
latex: Prefix label names with the specified -latex_prefix
This ensures names shared between multiple projects don't collide if
included in a common LaTeX document; cheri-architecture using both
sail-cheri-mips and sail-cheri-riscv runs into this.
Closes: #88
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions