Changes in kernel/arch/ia32/include/mm/asid.h [2ddcc7b:b3f8fb7] in mainline

File:

• kernel/arch/ia32/include/mm/asid.h (modified) (2 diffs)

kernel/arch/ia32/include/mm/asid.h

@@ -27 +27 @@
  */
 
-/** @addtogroup ia32mm
+/** @addtogroup ia32mm  
  * @{
  */
@@ -43 +43 @@
 #define KERN_ia32_ASID_H_
 
-#include <typedefs.h>
+#include <arch/types.h>
 
 typedef int32_t asid_t;
 
-#define ASID_MAX_ARCH  3
+#define ASID_MAX_ARCH           3
 
-#define asid_get()  (ASID_START + 1)
+#define asid_get()              (ASID_START + 1)
 #define asid_put(asid)