diff options
-rw-r--r-- | Build/source/texk/web2c/weave.ch | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Build/source/texk/web2c/weave.ch b/Build/source/texk/web2c/weave.ch index aca02c7ac1d..2bdbb6c04af 100644 --- a/Build/source/texk/web2c/weave.ch +++ b/Build/source/texk/web2c/weave.ch @@ -435,8 +435,7 @@ long_options[current_option].flag := address_of (no_xref); long_options[current_option].val := 1; incr (current_option); -@ -@<Global...@> = +@ @<Global...@> = @!no_xref:c_int_type; @ An element with all zeros always ends the list. |