[Commits] [wesnoth/wesnoth] f8b010: wmltools GUI: remove -f and -p wmllint options, ad...

[GitHub]

  Branch: refs/heads/1.12
  Home:   https://github.com/wesnoth/wesnoth
  Commit: f8b0103f0c0f4e18bd468b86f1822d08fc2d474b
      https://github.com/wesnoth/wesnoth/commit/f8b0103f0c0f4e18bd468b86f1822d08fc2d474b
  Author: Groggy Dice <groggydice at yahoo.com>
  Date:   2014-08-06 (Wed, 06 Aug 2014)

  Changed paths:
    M data/tools/GUI.pyw

  Log Message:
  -----------
  wmltools GUI: remove -f and -p wmllint options, add -m