[ fixes #1309 ] incorrect deprecation warning for _≤?_ in Data.Unit.Properties

MatthewDaggitt · MatthewDaggitt · commit 9b6c36b233cd · 2020-10-12T09:04:31.000+08:00
diff --git a/src/Data/Unit/Properties.agda b/src/Data/Unit/Properties.agda
@@ -125,7 +125,7 @@ infix 4 _≤?_
 _≤?_ : Decidable _≤_
 _ ≤? _ = yes _
 {-# WARNING_ON_USAGE _≤?_
-"Warning: _≤_ was deprecated in v1.2.
+"Warning: _≤?_ was deprecated in v1.2.
 Please use _≟_  instead."
 #-}
 ≤-isPreorder : IsPreorder _≡_ _≤_
