Agda 2.6.1 doesn't recognize it's terminating

src/plfa/part2/Properties.lagda.md

@@ -942,6 +942,7 @@ data Steps (L : Term) : Set where
 The evaluator takes gas and evidence that a term is well typed,
 and returns the corresponding steps:
 ```
+{-# TERMINATING #-}
 eval : ∀ {L A}
   → Gas
   → ∅ ⊢ L ⦂ A