Fix CI (#118)

CI was complaining about this missing import
avigad · Aug 28, 2023 · aa2f5e3 · aa2f5e3
1 parent e40d2ea
commit aa2f5e3
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/MIL.lean b/MIL.lean
@@ -31,3 +31,4 @@ import MIL.C09_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces
 import MIL.C10_Integration_and_Measure_Theory.S01_Elementary_Integration
 import MIL.C10_Integration_and_Measure_Theory.S02_Measure_Theory
 import MIL.C10_Integration_and_Measure_Theory.S03_Integration
+import MIL.Common