options menu size

[mcmahill mtl mit edu]

When I add an options menu to a table, it ends up being too small to read
when you're not accessing the menu.  Ie, the currently selected option can
t be read.  By either making other widgets in the same table column bigger
or by using set_usize on the options menu, I can get it big enough, but
this isn't so robust when different users choose different fonts.

So it seems as though the options menu isn't requesting enough size from
the table.

Any ideas how to fix this?

Thanks
-Dan