Dear Joris, Are you possibly implementing also the patch I suggested here:
http://savannah.gnu.org/bugs/?25938
It solves a minor but annoying problem for Gnome/Ubuntu users. Andrea _______________________________________________ Texmacs-dev mailing list [email protected] http://lists.gnu.org/mailman/listinfo/texmacs-dev
