X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=lib%2Futil.h;h=0101bf7b544d4bae1e3d7dc4535999cdcf8e9503;hb=77909859b05f0d2466069883306e8d75d280bbe7;hp=9e7b88f06825866358adca046f55108a6163b40a;hpb=29d4af6016b5616ccac56c702c078e36189ef951;p=openvswitch

diff --git a/lib/util.h b/lib/util.h
index 9e7b88f0..0101bf7b 100644
--- a/lib/util.h
+++ b/lib/util.h
@@ -127,6 +127,8 @@ int hexit_value(int c);
 
 char *dir_name(const char *file_name);
 
+void ignore(bool x UNUSED);
+
 #ifdef  __cplusplus
 }
 #endif