aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--test-suite/output/qualification.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index 3cf3c2d8fb..9300c3f546 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,3 +1,3 @@
-File "/home/pm/sources/coq/test-suite/output/qualification.v", line 19, characters 0-7:
+File "stdin", line 19, characters 0-7:
Error: Signature components for label test do not match: expected type
"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".