/*
 * Copyright (C) 2007 Bahadir Balban
 */
#ifndef __UTCB_H__
#define __UTCB_H__

#include <l4lib/types.h>
#include <l4lib/macros.h>
#include L4LIB_INC_ARCH(utcb.h)

int utcb_init(void);

#endif /* __UTCB_H__ */