Fix build

avigad · Sep 16, 2024 · 9daf81b · 9daf81b
1 parent 085d404
commit 9daf81b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C09_Linear_Algebra/S04_Bases.lean b/MIL/C09_Linear_Algebra/S04_Bases.lean
@@ -42,6 +42,7 @@ section matrices
 -- Multiplying matrices
 #eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![4, 6; 8, 10]
 
+-- QUOTE.
 /- TEXT:
 It is important to understand that this use of ``#eval`` is interesting only for
 exploration, it is not meant to replace a computer algebra system such as Sage.
@@ -86,7 +87,6 @@ Other familiar operations include the vector dot product,
 EXAMPLES: -/
 -- QUOTE:
 
--- QUOTE.
 /-
 TODO: make text for this section