RGBColor rgbFromHexName(string const & x11hexname)
{
RGBColor c;
- LASSERT(x11hexname.size() == 7 && x11hexname[0] == '#', /**/);
+ LASSERT(x11hexname.size() == 7 && x11hexname[0] == '#',
+ return c);
c.r = hexstrToInt(x11hexname.substr(1, 2));
c.g = hexstrToInt(x11hexname.substr(3, 2));
c.b = hexstrToInt(x11hexname.substr(5, 2));
{ Color_urllabel, N_("URL label"), "urllabel", "blue", "urllabel" },
{ Color_urltext, N_("URL text"), "urltext", "blue", "urltext" },
{ Color_depthbar, N_("depth bar"), "depthbar", "IndianRed", "depthbar" },
+ { Color_scroll, N_("scroll indicator"), "scroll", "IndianRed", "scroll" },
{ Color_language, N_("language"), "language", "Blue", "language" },
{ Color_command, N_("command inset"), "command", "black", "command" },
{ Color_commandbg, N_("command inset background"), "commandbg", "azure", "commandbg" },