#!/bin/bash

## builds the kernel and the mars module in the
## directories specified in default-make_mars.conf
## and installs in in /boot resp. /lib/modules of your
## work station

## WIP: the make install call in the kernel source directory
##      modifies grub.cfg of your work station. Though
##      we save and restore this file by calls to grub_prepare and grub_finish
## If your work station does not use grub, you have to provide a *.conf file
## to restore the boot information changed by "make install"

run_list="grub_prepare make_mars_run grub_finish"