Check copyright header in Rocq files.

If we ever add Verilog files, we can "or" both results, I guess.
This commit is contained in:
Cesar Strauss 2025-12-09 07:45:35 -03:00
parent e54558d848
commit e4210a672f
Signed by: cesar
SSH key fingerprint: SHA256:sJUl6USz0D6c6sAQyFZab8XNPJnT05pt2ES0Lv/hCg4

View file

@ -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"
;;