From f661fc17d7e512a3eab0255919796ea9af6d139d Mon Sep 17 00:00:00 2001
From: Artur Signell <artur@vaadin.com>
Date: Mon, 10 Sep 2012 19:21:55 +0300
Subject: [PATCH] Re-added old DefaultWidgetSet which was accidentally deleted
 in a merge

---
 .../src/com/vaadin/terminal/gwt/DefaultWidgetSet.gwt.xml | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 client/src/com/vaadin/terminal/gwt/DefaultWidgetSet.gwt.xml

diff --git a/client/src/com/vaadin/terminal/gwt/DefaultWidgetSet.gwt.xml b/client/src/com/vaadin/terminal/gwt/DefaultWidgetSet.gwt.xml
new file mode 100644
index 0000000000..f3cc2bca1c
--- /dev/null
+++ b/client/src/com/vaadin/terminal/gwt/DefaultWidgetSet.gwt.xml
@@ -0,0 +1,9 @@
+<module>
+    <!-- This GWT module is provided for backwards compatibility only. You 
+        should inherit com.vaadin.DefaultWidgetSet instead. -->
+
+    <!-- Hint for WidgetSetBuilder not to automatically update the file -->
+    <!-- WS Compiler: manually edited -->
+    <inherits name="com.vaadin.DefaultWidgetSet" />
+
+</module>
\ No newline at end of file
-- 
2.39.5