#!/bin/bash

# patch script/version.pf for distributions

# be a bit verbose in the comments
echo "# `whoami`@`hostname` - `date`" > script/version.pf

# official version name
echo \"$*\" >> script/version.pf