From e4210a672f6ff60139236fb000b35b08955e9fa8 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Tue, 9 Dec 2025 07:45:35 -0300
Subject: [PATCH] Check copyright header in Rocq files.

If we ever add Verilog files, we can "or" both results, I guess.
---
 scripts/check-copyright.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/scripts/check-copyright.sh b/scripts/check-copyright.sh
index 3651931..023cd21 100755
--- a/scripts/check-copyright.sh
+++ b/scripts/check-copyright.sh
@@ -32,6 +32,7 @@ POUND_HEADER=('^"# SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"# See Notice
 SLASH_HEADER=('^"// SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"// See Notices.txt for copyright information"$')
 MD_HEADER=('^"<!--"$' '^"SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"See Notices.txt for copyright information"$')
 JSON_HEADER=('^"{"$' '^"    \"license_header\": ["$' '^"        \"SPDX-License-Identifier: LGPL-3.0-or-later\","$' '^"        \"See Notices.txt for copyright information\""')
+ROCQ_HEADER=('^"(*  SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"   See Notices.txt for copyright information *)"$')
 
 function main()
 {
@@ -64,6 +65,9 @@ function main()
         *.json)
             check_file "$file" "${JSON_HEADER[@]}"
             ;;
+        *.v)
+            check_file "$file" "${ROCQ_HEADER[@]}"
+            ;;
         *)
             fail_file "$file" 0 "unimplemented file kind -- you need to add it to $0"
             ;;