From 17de7c785c921aef542681ee66538508d270fdf3 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 and rebased for stable branch. --- src/generator.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/generator.ml b/src/generator.ml index b2b3f83..a7673c1 100755 --- a/src/generator.ml +++ b/src/generator.ml @@ -7490,9 +7490,10 @@ and generate_fish_cmds () = List.iter ( function - | Device name | String name - | OptString name | FileIn name | FileOut name | Bool name - | Int name | Int64 name -> () + | Device _ | String _ + | OptString _ | Bool _ + | Int _ | Int64 _ + | FileIn _ | FileOut _ -> () | Pathname name | Dev_or_Path name -> pr " free (%s);\n" name | StringList name | DeviceList name -> -- 1.8.3.1