Removed definitions from level in filter

mmasdeu · Mar 4, 2022 · f2bc123 · f2bc123
1 parent 214a221
commit f2bc123
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/game_config.toml b/game_config.toml
@@ -37,11 +37,11 @@ levels = [ "src/separation_world/level*.lean" ]
 name = "Filter world"
 id = 6
 parents = [5]
-levels = [ "src/filter_world/*.lean"]
+levels = [ "src/filter_world/level*.lean"]
 
 [[worlds]]
 name = "Open and closed world"
 id = 7
 parents = [6]
-levels = [ "src/open_and_closed_world/*.lean"]
+levels = [ "src/open_and_closed_world/level*.lean"]