diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-11 21:57:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-11 21:57:14 +0000 |
commit | a25b07cd09b7723009acf4e95fe6575bac553fff (patch) | |
tree | b6e1c1b7536673c26b1e3640facf03a11ceb0a49 | |
parent | b7b76a7481bfe79fedb031ffa5694fa7dae62870 (diff) |
ensure using bash for new-theory script
-rwxr-xr-x | contrib/new-theory | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/new-theory b/contrib/new-theory index 6488eaec9..0045e7b41 100755 --- a/contrib/new-theory +++ b/contrib/new-theory @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # # usage: new-theory theory-directory-name # |