chore: Silence a warning that is not critical at all

erikmd · erikmd · commit 5e05f204fae6 · 2025-04-30T16:39:09.000+02:00
```
mathcomp/single/Dockerfile:2 DL3006 warning: Always tag the version of an image explicitly
```

Later, we could split the Dockerfile into 2 different ones instead if need be.
diff --git a/mathcomp/single/Dockerfile b/mathcomp/single/Dockerfile
@@ -1,4 +1,5 @@
 ARG COQ_TAG="dev"
+# hadolint ignore=DL3006
 FROM ${COQ_TAG}
 
 ARG MATHCOMP_VERSION="dev"

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,5 @@`
`1`	`1`	`ARG COQ_TAG="dev"`
	`2`	`+# hadolint ignore=DL3006`
`2`	`3`	`FROM ${COQ_TAG}`
`3`	`4`
`4`	`5`	`ARG MATHCOMP_VERSION="dev"`