Rodrigo Arias 118e451899 Fix config titles

2022-10-05 15:58:14 +02:00

..

kernel

Fix position, size and titles of configs

2022-10-05 15:25:41 +02:00

nanos6

Fix position, size and titles of configs

2022-10-05 15:25:41 +02:00

nodes

Fix config titles

2022-10-05 15:58:14 +02:00

nosv

Fix config titles

2022-10-05 15:58:14 +02:00

openmp

Fix config titles

2022-10-05 15:58:14 +02:00

ovni

Fix position, size and titles of configs

2022-10-05 15:25:41 +02:00

tampi

Fix config titles

2022-10-05 15:58:14 +02:00