#!/bin/csh
set echo
	chdir ~ksos/src/kernel/work ;			make $*
	chdir ~ksos/src/lib/kernel_interface/work ;	make $*
	chdir ~ksos/src/lib/nksr/work ;			make $*
#	chdir ~ksos/src/lib/kip/work ;			make $*
#	chdir ~ksos/src/lib/usr/work ;			make $*
	chdir ~ksos/lib/trusted ;			make $*
#	chdir ~ksos/lib/usr ;				make $*
	chdir ~ksos/src/unix/stc/work ;			make $*
	chdir ~ksos/src/nksr/boot0 ;			make $*
	chdir ~ksos/src/nksr/boot1 ;			make $*
	chdir ~ksos/src/nksr/init/work ;		make $*
	chdir ~ksos/src/nksr/PBB/work ;			make $*
	chdir ~ksos/src/nksr/SIP/work ;			make $*
	chdir ~ksos/src/nksr/UDM/work ;			make $*
	chdir ~ksos/src/nksr/ACP/work ;			make $*
	chdir ~ksos/src/nksr/SSD/work ;			make $*
	chdir ~ksos/src/nksr/SSP/work ;			make $*
	chdir ~ksos/src/nksr/ACPop/work ;		make $*
#	chdir ~ksos/src/nksr/LPD/work ;			make $*
#	chdir ~ksos/src/nksr/MCE/work ;			make $*
#	chdir ~ksos/src/nksr/PCE/work ;			make $*
#	chdir ~ksos/src/usr ;				make $*
