Fix testsuite.

coq · Aug 9, 2023 · 8a93c89 · 8a93c89
1 parent 30685ba
commit 8a93c89
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/test-suite/misc/coqdep-require-filter-categories/stderr.ref b/test-suite/misc/coqdep-require-filter-categories/stderr.ref
@@ -1 +1,3 @@
-*** Warning: in file fA.v, library nonexistent is required and has not been found in the loadpath!
+Warning: in file fA.v, library
+         nonexistent is required and has not been found in the loadpath!
+         [module-not-found,filesystem,default]
diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps
@@ -1,3 +1,5 @@
-*** Warning: in file misc/external-deps/file1.v, external file d1 is required from root foo.bar and has not been found in the loadpath!
+Warning: in file misc/external-deps/file1.v, external file d1 is required
+         from root foo.bar and has not been found in the loadpath!
+         [module-not-found,filesystem,default]
 misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v 
 misc/external-deps/file1.vio: misc/external-deps/file1.v 
diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps
@@ -1,3 +1,5 @@
-*** Warning: in file misc/external-deps/file2.v, external file d1 is required from root foo.bar and has not been found in the loadpath!
+Warning: in file misc/external-deps/file2.v, external file d1 is required
+         from root foo.bar and has not been found in the loadpath!
+         [module-not-found,filesystem,default]
 misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v 
 misc/external-deps/file2.vio: misc/external-deps/file2.v