From 354c53de79366c09f8550b8cd23ebddb0b7d2c2f Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 27 Aug 2015 20:25:37 -0700
Subject: Add a tip to the packaging script

---
 package.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'package.py')

diff --git a/package.py b/package.py
index 62f8dbdf..fa111ec5 100644
--- a/package.py
+++ b/package.py
@@ -163,7 +163,7 @@ def run(cmd):
     flush("    + {}...".format(" ".join(cmd)), end=' ')
     retv = subprocess.call(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
     if retv != 0:
-        flush("failed!")
+        flush("failed! (Is Dafny or the Dafny server running?)")
         sys.exit(1)
     else:
         flush("done!")
-- 
cgit v1.2.3