#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
cd $DIR

make -C../kernel/ bench
../utils/other/retip > ../distro/customroot/etc/retip
./boot "$@"