Fix benchmark generation
Compare changes
@@ -18,6 +18,43 @@ void dummy(void *);
@@ -18,6 +18,43 @@ void dummy(void *);
@@ -28,11 +65,14 @@ int main(int argc, char **argv)
@@ -28,11 +65,14 @@ int main(int argc, char **argv)
@@ -69,18 +109,18 @@ int main(int argc, char **argv)
@@ -69,18 +109,18 @@ int main(int argc, char **argv)
@@ -105,4 +145,13 @@ int main(int argc, char **argv)
@@ -105,4 +145,13 @@ int main(int argc, char **argv)