diff options
Diffstat (limited to 'write_makefile.sh')
-rwxr-xr-x | write_makefile.sh | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/write_makefile.sh b/write_makefile.sh new file mode 100755 index 0000000..118635b --- /dev/null +++ b/write_makefile.sh @@ -0,0 +1,21 @@ +#!/bin/sh + +# This file is part of Haketilo +# +# Copyright (C) 2021, jahoti +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the CC0 1.0 Universal License as published by +# the Creative Commons Corporation. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# CC0 1.0 Universal License for more details. + +if [ ! -e record.conf ]; then + echo "Record of configuration 'record.conf' does not exist." >&2 + exit 1 +fi + +sed '/^# Configuration goes here$/r record.conf' < Makefile.in > Makefile |