Commit 2025-09-02 20:05 2d012532

View on Github →

chore: add deprecated modules (#29209) These modules were renamed in #28948 and #28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 Data.{Complex, Real}.xxx files that have been renamed to Analysis.{Complex, Real}.xxx. I had forgotten about running lake exe mk_all after the deprecated modules had been generated.

Estimated changes