diff options
author | Jonas Kohl | 2024-11-07 17:59:09 +0100 |
---|---|---|
committer | Jonas Kohl | 2024-11-07 17:59:09 +0100 |
commit | 0f4328e1713dfea73e82c91a3ca194d734416fe3 (patch) | |
tree | 8e729d639eada93c6bc4e46fada3b02885efd75d /generate-status-object.php | |
parent | bf940e4049ea39dc84f6c837bba094ba441cc491 (diff) |
Dockerize whole application
Diffstat (limited to 'generate-status-object.php')
-rw-r--r-- | generate-status-object.php | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/generate-status-object.php b/generate-status-object.php deleted file mode 100644 index 9d19070..0000000 --- a/generate-status-object.php +++ /dev/null @@ -1,30 +0,0 @@ -<?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; |