/*
 * system_timer.h
 *
 *  Created on: Dec 6, 2017
 *      Author: maximilian
 */

#ifndef PLATFORM_SYSTEM_TIMER_H_
#define PLATFORM_SYSTEM_TIMER_H_

void initClock(void);

#endif /* PLATFORM_SYSTEM_TIMER_H_ */