#!/bin/bash # Generate HTML header # # Copyright (C) 2019 Mike Gerwitz # # This program is free software: you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by # the Free Software Foundation, either version 3 of the License, or # (at your option) any later version. # # 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 # GNU General Public License for more details. # # You should have received a copy of the GNU General Public License # along with this program. If not, see . # # The header is mostly static but contains a dynamic page type and title. ## set -euo pipefail declare -ri EX_USAGE=64 # Generate header by populating @PAGE_{TITLE,TYPE}@. If no title is given, # then the title will be completely omitted. If provided, it will have an # em dash delimiter appended, with whitespace on both sides for visual # clarity (contrary to my usual typographical conventions). main() { local -r type=${1?Missing type} local -r title_orig=${2:-} local -r title=${title_orig/&/\\&} [[ $type =~ ^[a-z]+$ ]] || { echo 'error: type must be an all-lowercase word' exit $EX_USAGE } [[ ! $title =~ \# ]] || { echo "error: title must not contain \`#'" exit $EX_USAGE } sed "s#@PAGE_TITLE@#$title${title:+ \\— }#g s#@PAGE_TYPE@#$type#g /