From d26ca1ba5cd99f3185947d17f4dd5578349bfebe Mon Sep 17 00:00:00 2001
From: Eddie Kohler <ekohler@gmail.com>
Date: Wed, 20 Dec 2023 16:53:02 -0500
Subject: [PATCH] Add batch/fileinfo script.

---
 batch/fileinfo.php | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 batch/fileinfo.php

diff --git a/batch/fileinfo.php b/batch/fileinfo.php
new file mode 100644
index 0000000000..b176416f8e
--- /dev/null
+++ b/batch/fileinfo.php
@@ -0,0 +1,43 @@
+<?php
+// fixdelegation.php -- HotCRP paper export script
+// Copyright (c) 2006-2022 Eddie Kohler; see LICENSE.
+
+if (realpath($_SERVER["PHP_SELF"]) === __FILE__) {
+    require_once(dirname(__DIR__) . "/src/init.php");
+    exit(Fileinfo_Batch::make_args($argv)->run());
+}
+
+class Fileinfo_Batch {
+    /** @var list<string> */
+    public $files = [];
+
+    /** @return int */
+    function run() {
+        if (empty($this->files)) {
+            $this->files[] = "-";
+        }
+        foreach ($this->files as $file) {
+            if ($file === "-") {
+                $content = stream_get_contents(STDIN);
+            } else {
+                $content = file_get_contents($file);
+            }
+            fwrite(STDOUT, sprintf("%-39s %s\n", $file, json_encode(Mimetype::content_info($content))));
+        }
+        return 0;
+    }
+
+    /** @param list<string> $argv
+     * @return Fileinfo_Batch */
+    static function make_args($argv) {
+        $arg = (new Getopt)->long(
+            "help,h !"
+        )->description("Report HotCRP-derived file info.
+Usage: php batch/fileinfo.php FILES...")
+         ->helpopt("help")
+         ->parse($argv);
+        $fib = new Fileinfo_Batch();
+        $fib->files = $arg["_"];
+        return $fib;
+    }
+}