« Previous | Next » 

Revision 7c132ef3

ID7c132ef3204771ee93c4ef31b5ee6aea36cf7b33

Added by Kostas Papadimitriou over 9 years ago

ui: Remove options menu from header

Files

  • added
  • modified
  • copied
  • renamed
  • deleted

View differences