aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-10-17 17:37:15 +0200
committerPierre-Marie Pédrot2016-10-17 17:37:15 +0200
commit48b342ed5b9fb514961e10b2684243dc0b4078be (patch)
treea412f7e12bf9592421d27a7263fd19e9f78a6188
parent409bc943e8d8a0bc0d35ae63f3530b7324ca975e (diff)
Fix output test for module qualification.
The output was embedding local paths from my machine.
-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".