diff options
Diffstat (limited to 'src')
-rwxr-xr-x | src/generator.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/generator.ml b/src/generator.ml index 6ef85fd6..2fb3f48e 100755 --- a/src/generator.ml +++ b/src/generator.ml @@ -7971,10 +7971,10 @@ and generate_fish_cmds () = List.iter ( function - | Device name | String name - | OptString name | Bool name - | Int name | Int64 name - | BufferIn name -> () + | Device _ | String _ + | OptString _ | Bool _ + | Int _ | Int64 _ + | BufferIn _ -> () | Pathname name | Dev_or_Path name | FileOut name -> pr " free (%s);\n" name | FileIn name -> |