--- a/src/Doc/prepare_document Tue Sep 10 11:46:51 2013 +0200 +++ b/src/Doc/prepare_document Tue Sep 10 11:57:53 2013 +0200 @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -e