There are some things that I realized while I was doing the port. I will mention them here:
There are some things that I realized while I was doing the port. I will mention them here:
−
* Gtk.Widget.hide_all() doesn't exist anymore. We should use just <tt>.hide</tt>: http://developer.gnome.org/gtk3/3.5/GtkWidget.html#gtk-widget-hide
+
* <tt>Gtk.Widget.hide_all()</tt> doesn't exist anymore. We should use just <tt>.hide</tt>: http://developer.gnome.org/gtk3/3.5/GtkWidget.html#gtk-widget-hide