build script needs bash
authorAdam Chlipala <adamc@hcoop.net>
Sun, 6 Apr 2008 16:30:52 +0000 (16:30 +0000)
committerAdam Chlipala <adamc@hcoop.net>
Sun, 6 Apr 2008 16:30:52 +0000 (16:30 +0000)
build

diff --git a/build b/build
index 24c1c56..db4d64f 100755 (executable)
--- a/build
+++ b/build
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 source settings