aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--test-suite/Makefile2
-rw-r--r--test-suite/csdp.cachebin45137 -> 76555 bytes
2 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index fcf137ca1f..4e94f29a07 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -371,7 +371,7 @@ misc/xml.log:
else \
echo $(log_success); \
echo " misc/xml...apparently ok"; \
- fi; rm -r misc/xml; \
+ fi; rm -rf misc/xml; \
} > "$@"
# Check that both coqdep and coqtop/coqc takes the later -I/-R
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 7874f46954..297ac255d3 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
Binary files differ