X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fhelper.h;h=d388ccb41821b132afaf5670647ea3dd961a0cd4;hb=b6bcae693f035491ae0625f301f3e630c1335555;hp=d08a17526bc59e6389d3d1ac996c1711238a7728;hpb=9bf1c33953f7feff2a24a06293f6fe96b75cc41a;p=pspp

diff --git a/src/ui/gui/helper.h b/src/ui/gui/helper.h
index d08a17526b..d388ccb418 100644
--- a/src/ui/gui/helper.h
+++ b/src/ui/gui/helper.h
@@ -26,6 +26,10 @@
 #include <gtk/gtk.h>
 #include <glade/glade.h>
 
+
+
+void paste_syntax_in_new_window (const gchar *syntax);
+
 /*
    GtkRecentChooserMenu was added in 2.10.0
    but it didn't support GtkRecentFilters until