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/sail.ml | |
| 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/sail.ml')
| -rw-r--r-- | src/sail.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sail.ml b/src/sail.ml index d07ea216..53a5cc5d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -162,7 +162,7 @@ let options = Arg.align ([ " pretty print the input to LaTeX"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix := prefix), - "<prefix> set a custom prefix for generated LaTeX macro command (default sail)"); + "<prefix> set a custom prefix for generated LaTeX labels and macro commands (default sail)"); ( "-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output"); |