From 8a93c89efac87e0decb6b083ffaff8afb4629099 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 9 Aug 2023 13:57:47 +0200 Subject: [PATCH] Fix testsuite. --- test-suite/misc/coqdep-require-filter-categories/stderr.ref | 4 +++- test-suite/misc/external-deps/file1.notfound.deps | 4 +++- test-suite/misc/external-deps/file2.notfound.deps | 4 +++- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/test-suite/misc/coqdep-require-filter-categories/stderr.ref b/test-suite/misc/coqdep-require-filter-categories/stderr.ref index d324d8ca99b04..c83fb7a445a5f 100644 --- 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 index 5a6f45cc4950e..5985cbc7b3350 100644 --- 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 index 07d683a83a81b..ae49c0228372a 100644 --- 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