diff options
Diffstat (limited to 'Build/source/texk/web2c/pltotf.ch')
-rw-r--r-- | Build/source/texk/web2c/pltotf.ch | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/Build/source/texk/web2c/pltotf.ch b/Build/source/texk/web2c/pltotf.ch index 575d31b3e27..d877353e73f 100644 --- a/Build/source/texk/web2c/pltotf.ch +++ b/Build/source/texk/web2c/pltotf.ch @@ -333,12 +333,10 @@ long_options[current_option].flag := address_of (verbose); long_options[current_option].val := 1; incr (current_option); -@ -@<Glob...@> = +@ @<Glob...@> = @!verbose: c_int_type; -@ -@<Initialize the option...@> = +@ @<Initialize the option...@> = verbose := false; @ An element with all zeros always ends the list. |