From 881f8bbb7358e74507ae03394ff0d0715bd5453f Mon Sep 17 00:00:00 2001
From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sun, 19 Aug 2012 13:19:17 -0700
Subject: [PATCH] widgets: #include missing header file.

It didn't build for me otherwise.
---
 src/ui/gui/widgets.c | 2 ++
 1 file changed, 2 insertions(+)

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"
 
 
-- 
2.30.2