librace: format DEBUG() prints properly

[c11tester.git] / userprog.c

diff --git a/userprog.c b/userprog.c
index c90ad1e8151c7fcb7945bb9e49cde67303e05a23..4b106d88c11e8f0829008b5d7c47dd626e093c05 100644 (file)
--- a/userprog.c
+++ b/userprog.c
@@ -26,8 +26,8 @@ void user_main()
        atomic_int obj;
 
        printf("Creating 2 threads\n");
-       thrd_create(&t1, (void (*)())&a, &obj);
-       thrd_create(&t2, (void (*)())&a, &obj);
+       thrd_create(&t1, (thrd_start_t)&a, &obj);
+       thrd_create(&t2, (thrd_start_t)&a, &obj);
 
        thrd_join(t1);
        thrd_join(t2);