Commit 2024-06-01 12:47 bffb043c

refactor: tweak and move functionality for getting all modules out of scripts (#13339) With #13245, two scripts in scripts would like to use very similar information: move it to a central place instead (a file in Mathlib/Util). Suggestions for better locations are welcome! Also, split the getAll function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd.

• depends on: #11853 which adds these utility functions