# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1716918669 -7200
# Node ID 03c058592c58167a9fb235973aa6e42645f79b84
# Parent  6ac48d53d371c5cb7e6fc012894eee047b68d4d0
add explicit Content-Length header to http response (otherwise it is missing in HEAD responses);

diff -r 6ac48d53d371 -r 03c058592c58 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Tue May 28 19:49:42 2024 +0200
+++ b/src/Pure/General/http.scala	Tue May 28 19:51:09 2024 +0200
@@ -222,6 +222,7 @@
 
     def write(http: HttpExchange, code: Int, is_head: Boolean = false): Unit = {
       http.getResponseHeaders.set("Content-Type", content_type)
+      http.getResponseHeaders.set("Content-Length", output.length.toString)
       http.sendResponseHeaders(code, if (is_head) -1 else output.length.toLong)
       if (!is_head) using(http.getResponseBody)(output.write_stream)
     }