#!/bin/sh
# This script will produce a platform specific string to stdout.
# It is used by Makefile

if [ `uname -s` == Linux ]
then
    echo -n "linux_"
    gcc -dumpmachine | sed s/-.*//
else
    echo "Error: Unknown platform! "1>&2
    exit 2
fi
