author | wenzelm |
Mon, 20 Mar 2023 11:13:01 +0100 | |
changeset 77694 | ea509b0bfc80 |
parent 77693 | 068ff989c143 |
child 77695 | 93531ba2c784 |
child 77930 | 84a09beb682d |
--- 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