overlay

Tragicus · Tragicus · commit f3688c001d20 · 2025-06-19T15:03:41.000+02:00
diff --git a/dev/ci/user-overlays/20730-Tragicus-reduce-projs.sh b/dev/ci/user-overlays/20730-Tragicus-reduce-projs.sh
@@ -0,0 +1 @@
+overlay metarocq https://github.com/Tragicus/metacoq rocq20730 20730

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+overlay metarocq https://github.com/Tragicus/metacoq rocq20730 20730`