Pixl.js Menu Font size

The Pixl.js menu code is basically a wrapper around graphical_menu that adds the icons and button support, so you should be able to use the functionality from there like fontHeight: http://www.espruino.com/graphical_menu

However Pixl.menu tries to reset the font when it starts, so you have to use Pixl.menu, then set the font, then re-render - but otherwise it works:

var mainmenu = {
  "" : {
    "title" : "-- Main Menu --",
    "fontHeight" : 12
  },
  "Backlight On" : function() { LED1.set(); },
  "Backlight Off" : function() { LED1.reset(); },
  "Exit" : function() { Pixl.menu(); },
};

require("Font8x12").add(Graphics);
m=Pixl.menu(mainmenu);
g.setFont8x12();
m.draw();

If I added a predraw option for graphical_menu then it'd be tidier though - you could just set the font in that...

edit: just added predraw, so versions of Pixl.js after 1v99 will have that in and:

var mainmenu = {
  "" : {
    "title" : "-- Main Menu --",
    "fontHeight" : 12,
    "predraw": function(g) {g.setFont8x12();}
  },
  "Backlight On" : function() { LED1.set(); },
  "Backlight Off" : function() { LED1.reset(); },
  "Exit" : function() { Pixl.menu(); },
};
require("Font8x12").add(Graphics);
m=Pixl.menu(mainmenu);

should work