diff options
| author | Robert Norton | 2018-05-10 17:40:48 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-10 17:40:48 +0100 |
| commit | 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d (patch) | |
| tree | 393b217b376022500b1bfc5ec73f53da30722962 /lib/main.ml | |
| parent | 938f06bc6c711ef3e777beaace7da8d4aee158b9 (diff) | |
latex: don't include the prefix in the label. This means we have the option of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
Diffstat (limited to 'lib/main.ml')
0 files changed, 0 insertions, 0 deletions