old_pretimeout   1009 drivers/char/ipmi/ipmi_watchdog.c 		int old_pretimeout = pretimeout;
old_pretimeout   1040 drivers/char/ipmi/ipmi_watchdog.c 		pretimeout = old_pretimeout;