From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sat, 12 Sep 2015 18:31:38 +0000 (-0700)
Subject: gui: Mark print_startup_time() unused to avoid warning.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=14125d13946c1b2c3b7efe6cb88e35aa4623210b;p=pspp

gui: Mark print_startup_time() unused to avoid warning.
---

diff --git a/src/ui/gui/main.c b/src/ui/gui/main.c
index d2513e8ec8..d1a4798fd1 100644
--- a/src/ui/gui/main.c
+++ b/src/ui/gui/main.c
@@ -160,7 +160,7 @@ startup_option_callback (int id, void *show_splash_)
     }
 }
 
-static gboolean
+static gboolean UNUSED
 print_startup_time (gpointer data)
 {
   g_timer_stop (startup);