Merge branch 'master' into jgrpp

# Conflicts: # src/industry_gui.cpp # src/lang/korean.txt # src/town.h # src/town_gui.cpp
2020-01-08 18:40:34 +00:00
parent 6d326deafe 5a31efd98d
commit 4adfe0c9ae
73 changed files with 210 additions and 249 deletions
--- a/src/core/pool_type.hpp
+++ b/src/core/pool_type.hpp
@@ -12,7 +12,6 @@

 #include "smallvec_type.hpp"
 #include "enum_type.hpp"
-#include <functional>

 /** Various types of a pool. */
 enum PoolType {