Michael Zeising - 2010-03-30
  • labels: --> Tools
  • priority: 5 --> 7
  • assigned_to: nobody --> m_zeising
  • summary: MakeIndex option --> Add makeindex to the tools