#!/bin/sh

# Very simple script to copy the global hosts file over the local one
# while preserving the localhost entry.  Run on DETER master clients

grep 127\\.0\\.0\\.1 /etc/hosts > /tmp/hosts
cat $1 >> /tmp/hosts
cp /tmp/hosts /etc/hosts && rm /tmp/hosts
