# HG changeset patch
# User wenzelm
# Date 1573744924 -3600
# Node ID 557703db74c33e3c39a2e11c5deae8e2717c3b9d
# Parent  f79006c533b09b1acdf89d3e23c1f062f382c265
tuned PHP setup;

diff -r f79006c533b0 -r 557703db74c3 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Thu Nov 14 16:07:34 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Thu Nov 14 16:22:04 2019 +0100
@@ -316,7 +316,8 @@
     File.write(php_conf,
       "post_max_size = 32M\n" +
       "opcache.validate_timestamps = 0\n" +
-      "memory_limit = 512M\n")
+      "memory_limit = 512M\n" +
+      "max_execution_time = 120\n")
 
 
     /* Apache setup */