From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sun, 19 Aug 2012 20:19:17 +0000 (-0700)
Subject: widgets: #include missing header file.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=881f8bbb7358e74507ae03394ff0d0715bd5453f;p=pspp

widgets: #include missing header file.

It didn't build for me otherwise.
---

diff --git a/src/ui/gui/widgets.c b/src/ui/gui/widgets.c
index 008d37e52a..c4f8099067 100644
--- a/src/ui/gui/widgets.c
+++ b/src/ui/gui/widgets.c
@@ -1,5 +1,7 @@
 #include <config.h>
 
+#include <gtksourceview/gtksourceview.h>
+
 #include "widgets.h"