#!/bin/sh
# usage: definepath top_srcdir prefix pp-symbol path
#
# Emit '#define pp-symbol "path"', where a leading prefix of path is removed.
echo '#define '$3'                   "'"`$1/scripts/unprefix "$2" "$4"`"'"' \
| sed 's/\(........................... \) *"/\1"/'