Topic: Almost empty top folders
Yaël Dillies (Nov 20 2021 at 18:13):
testing both have very little content (1 and 4 files respectively). Are people opposed to renaming
data.random and move everything in
Scott Morrison (Nov 20 2021 at 23:44):
I would guess
testing/slim_check is not under either
test because @Simon Hudon arranged so that it was all non-meta code.
Scott Morrison (Nov 20 2021 at 23:45):
One thing to consider is what will happen to it during the port to Lean 4. If it is under
test it won't be automatically translated. (We could still run mathport on it, but it won't be part of the automatic workflow.)
Yaël Dillies (Nov 20 2021 at 23:47):
I think either is low priority, so you tell me.
Last updated: Aug 03 2023 at 10:10 UTC