src/Pure/Tools/phabricator.scala
changeset 71328 4642a81f5913
parent 71326 d85258458623
child 71330 836fde6f9d7e
equal deleted inserted replaced
71327:a89729bdde89 71328:4642a81f5913
   381 
   381 
   382     val dump_name = isabelle_phabricator_name(name = "dump")
   382     val dump_name = isabelle_phabricator_name(name = "dump")
   383     command_setup(dump_name, body =
   383     command_setup(dump_name, body =
   384 """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
   384 """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
   385 [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
   385 [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
   386 echo "Creating $ROOT/database/dump.sql.gz"
   386 echo -n "Creating $ROOT/database/dump.sql.gz ..."
   387 "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' """)
   387 "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure'
       
   388 echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """)
   388 
   389 
   389 
   390 
   390     /* Phabricator upgrade */
   391     /* Phabricator upgrade */
   391 
   392 
   392     command_setup(isabelle_phabricator_name(name = "upgrade"),
   393     command_setup(isabelle_phabricator_name(name = "upgrade"),
   469 
   470 
   470     config.execute("config set phabricator.base-uri " + Bash.string(server_url))
   471     config.execute("config set phabricator.base-uri " + Bash.string(server_url))
   471 
   472 
   472     Linux.service_restart("apache2")
   473     Linux.service_restart("apache2")
   473 
   474 
   474     progress.echo("\nWeb configuration via " + server_url)
   475     progress.echo("\nFurther manual configuration via " + server_url)
   475 
   476 
   476 
   477 
   477     /* PHP daemon */
   478     /* PHP daemon */
   478 
   479 
   479     progress.echo("\nPHP daemon setup ...")
   480     progress.echo("\nPHP daemon setup ...")