From a5e110c163c134277b975f2c93c221e52554ec28 Mon Sep 17 00:00:00 2001 From: Richard Jones Date: Wed, 21 Jul 2010 12:52:10 +0100 Subject: [PATCH] generator: Remove unnecessary parameter. The 'name' parameter is not used on the right hand side of the match, so it can be removed. (cherry picked from commit 2e7da2a2f3bbc6d6db148d7dc2ce238bf56f34db) --- src/generator.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/generator.ml b/src/generator.ml index d427558..3ee4b8b 100755 --- a/src/generator.ml +++ b/src/generator.ml @@ -7930,10 +7930,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 -> -- 1.8.3.1