Root/common/Makefile.title

Source at commit e324adc35a0c28aeabe6366bba9e36fd9653298a created 11 years 3 months ago.
By Werner Almesberger, add title pages to the catalogs, with useful information like the creation date
1SHELL = /bin/bash
2
3COMMIT_DATE := $(shell date -u +'%F %T UTC' \
4    -d "`git show --pretty=format:'%ci' | sed q`")
5GIT_HASH := $(shell git rev-parse HEAD)
6GIT_STATUS := $(shell [ -z "`git status -s -uno`" ] || echo +)
7
8title.ps: ../common/title.fig
9        fig2dev -L ps $< | \
10            sed -e "s|<TITLE-NAME>|$(TITLE_NAME)|" \
11            -e "s/<DATE>/`date -u +'%F %T UTC'`/" \
12                -e "s/<HEAD-HASH>/$(GIT_HASH)$(GIT_STATUS)/" \
13                -e "s/<HEAD-DATE>/$(COMMIT_DATE)/" \
14            -e "s|<TITLE-FILE>|$(TITLE_FILE)|" >$@; \
15        [ "$${PIPESTATUS[*]}" = "0 0" ] || { rm -f $@ exit 1; }
16

Archive Download this file

Branches:
master



interactive