# HG changeset patch
# User wenzelm
# Date 1679307181 -3600
# Node ID ea509b0bfc80723d2631c374be9d3e4f443c25ba
# Parent  068ff989c143ea5c223e833f3f7fd912aa82a224
more operations;

diff -r 068ff989c143 -r ea509b0bfc80 src/Pure/General/space.scala
--- 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