Fiasco: jdb_tcb.h Source File

00001 // AUTOMATICALLY GENERATED -- DO NOT EDIT!         -*- c++ -*-
00002 
00003 #ifndef jdb_tcb_h
00004 #define jdb_tcb_h
00005 
00006 #include "l4_types.h"
00007 
00008 //
00009 // INTERFACE definition follows 
00010 //
00011 
00012 
00013 int jdb_show_tcb(L4_uid tid, int level);
00014 
00015 #endif // jdb_tcb_h