various fixes

This commit is contained in:
2017-01-20 01:54:11 +01:00
parent 7d54956ba2
commit ded9ac9fb9
13 changed files with 59 additions and 2 deletions

View File

@ -1,5 +1,10 @@
#!/bin/bash
# This file is part of Jehanne.
#
# Copyright (C) 2016-2017 Giacomo Tesio <giacomo@tesio.it>
if [ "$JEHANNE" = "" ]; then
echo $0 requires the shell started by ./hacking/devshell.sh
exit 1