#ifdef HAVE_CONFIG_H
#  include <config.h>
#endif

#include <gtk/gtk.h>

#include "manual_callbacks.h"
#include "manual.h"
#include "support.h"
#include "global.h"


void
on_close_manual_button_clicked         (GtkButton       *button,
                                        gpointer         user_data)
{

	gtk_widget_destroy(manual_window);
	gtk_widget_set_sensitive(manual,TRUE);
}

gboolean
on_manual_window_delete_event          (GtkWidget       *widget,
                                        GdkEvent        *event,
                                        gpointer         user_data)
{
	gtk_widget_destroy(manual_window);
	gtk_widget_set_sensitive(manual,TRUE);
	return TRUE;
  	
}