[Widelands-dev] [Merge] lp:~widelands-dev/widelands/bug-1380307 into lp:widelands

The proposal to merge lp:~widelands-dev/widelands/bug-1380307 into lp:widelands has been updated. Status: Needs review = Merged For more details, see: https://code.launchpad.net/~widelands-dev/widelands/bug-1380307/+merge/238083 -- https://code.launchpad.net/~widelands-dev/widelands/bug

[Widelands-dev] [Merge] lp:~widelands-dev/widelands/bug-1380307 into lp:widelands

, and will be probably removed sometimes in the future. -- https://code.launchpad.net/~widelands-dev/widelands/bug-1380307/+merge/238083 Your team Widelands Developers is requested to review the proposed merge of lp:~widelands-dev/widelands/bug-1380307 into lp:widelands. === modified file 'src/ai

Re: [Widelands-dev] [Merge] lp:~widelands-dev/widelands/bug-1380307 into lp:widelands

Review: Approve -- https://code.launchpad.net/~widelands-dev/widelands/bug-1380307/+merge/238083 Your team Widelands Developers is subscribed to branch lp:~widelands-dev/widelands/bug-1380307. ___ Mailing list: https://launchpad.net/~widelands-dev