diff --git a/vir/build.rs b/vir/build.rs
index 1cb55772c..506ec3b4e 100644
--- a/vir/build.rs
+++ b/vir/build.rs
@@ -20,7 +20,15 @@ fn main() {
         // so that one could do `clippy --fix`...
         "#[allow(clippy::uninlined_format_args)]".to_string(),
         "#[rustfmt::skip]".to_string(),
-        format!("#[path = \"{}\"]", gen_dir.join("mod.rs").display()),
+        // Escape "\" as "\\", especially for Windows
+        format!(
+            "#[path = \"{}\"]",
+            gen_dir
+                .join("mod.rs")
+                .display()
+                .to_string()
+                .replace('\\', "\\\\")
+        ),
         "mod gen;".to_string(),
     ]
     .join("\n");