diff options
Diffstat (limited to 'generate-status-object.php')
-rw-r--r-- | generate-status-object.php | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/generate-status-object.php b/generate-status-object.php new file mode 100644 index 0000000..9d19070 --- /dev/null +++ b/generate-status-object.php @@ -0,0 +1,30 @@ +<?php + +if (empty($argv[1])) { + file_put_contents("php://stderr", "No runner ID specified"); + exit(1); +} + +define("WORK_DIR", __DIR__ . "/_runners/" . $argv[1] . "/results"); + +function get(string $name): ?string { + $file = WORK_DIR . "/" . $name; + if (!is_file($file)) + return null; + return file_get_contents($file); +} + +$data = [ + "compile" => [ + "status" => get("c.s"), + "stdout" => get("c.0"), + "stderr" => get("c.1"), + ], + "run" => [ + "status" => get("r.s"), + "stdout" => get("r.0"), + "stderr" => get("r.1"), + ], +]; + +echo json_encode($data, JSON_UNESCAPED_SLASHES | JSON_PRETTY_PRINT) . PHP_EOL; |