Merging latest develop commits

2019-07-16 11:20:24 +02:00
parent 45f5bdd38f 3c85cd58b4
commit 2b321fd1c7
355 changed files with 13082 additions and 594202 deletions
@@ -911,7 +911,6 @@ int main(int argc, char **argv) {

  if (help)
    exit(0);
-
  if (thread_struct.parallel_conf != PARALLEL_SINGLE_THREAD)
    set_worker_conf("WORKER_ENABLE");