aboutsummaryrefslogtreecommitdiff
path: root/runtest.exp
diff options
context:
space:
mode:
Diffstat (limited to 'runtest.exp')
-rw-r--r--runtest.exp3
1 files changed, 2 insertions, 1 deletions
diff --git a/runtest.exp b/runtest.exp
index 5ced8ab..6126254 100644
--- a/runtest.exp
+++ b/runtest.exp
@@ -867,7 +867,8 @@ if {[info exists env(DEJAGNU)]} {
# config file, but issue an error if $DEJAGNU is erroneously defined.
# Since $DEJAGNU is set there is *supposed* to be a global config file,
# so the current behaviour seems reasonable.
- send_error "WARNING: global config file $env(DEJAGNU) not found.\n"
+ send_error "ERROR: global config file $env(DEJAGNU) not found.\n"
+ exit 1
}
if {![info exists boards_dir]} {
set boards_dir "[file dirname $env(DEJAGNU)]/boards"