
#include <rtl_conf.h>
#include <rtl_sched.h>
#include <rtl_core.h>

#ifdef CONFIG_RTL_FP_SUPPORT
extern inline int is_set_TS(void)
{
	int current_TS;
	return current_TS;
}


extern inline void rtl_fpu_save (schedule_t *s, RTL_THREAD_STRUCT *current_t)
{
	__asm("\n");
}


extern inline void rtl_fpu_restore (schedule_t *s,RTL_THREAD_STRUCT *current_t) {
	__asm("\n");

	
}


extern inline void rtl_task_init_fpu (RTL_THREAD_STRUCT *t, RTL_THREAD_STRUCT *fpu_owner)
{
	__asm("\n");
	
}

#endif /* CONFIG_RTL_FP_SUPPORT */

