| changeset 77694 | ea509b0bfc80 |
| parent 77687 | 07e2cafcc97e |
| child 77708 | f137bf5d3d94 |
--- a/src/Pure/General/space.scala Mon Mar 20 11:09:51 2023 +0100 +++ b/src/Pure/General/space.scala Mon Mar 20 11:13:01 2023 +0100 @@ -31,6 +31,7 @@ def + (other: Space): Space = new Space(bytes + other.bytes) def - (other: Space): Space = new Space(bytes - other.bytes) def * (scalar: Double): Space = new Space((bytes * scalar).round) + def / (other: Space): Double = B / other.B def is_proper: Boolean = bytes > 0 def is_relevant: Boolean = MiB >= 1.0