diff options
Diffstat (limited to 'Build/source/texk/web2c/pooltype.ch')
-rw-r--r-- | Build/source/texk/web2c/pooltype.ch | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Build/source/texk/web2c/pooltype.ch b/Build/source/texk/web2c/pooltype.ch index f93b7bb7c46..55e8a65bd8b 100644 --- a/Build/source/texk/web2c/pooltype.ch +++ b/Build/source/texk/web2c/pooltype.ch @@ -68,7 +68,7 @@ end. @y @!pool_file:packed file of text_char; {the string-pool file output by \.{TANGLE}} -@!pool_name:^char; +@!pool_name:const_c_string; @z % The name of the pool file is dynamically determined. We open it at the |