Add comment.
[pintos-anon] / src / devices / timer.h
index ba736d2a28d6d7e23c9ce41d4da06006f2877554..5807b0fb253d1dace47cd211990b0cc6d4dffe99 100644 (file)
@@ -3,6 +3,7 @@
 
 #include <stdint.h>
 
+/* Number of timer interrupts per second. */
 #define TIMER_FREQ 100
 
 void timer_init (void);