From b708eaec2cf785caac175d9bfeefcde4927e00cb Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Sat, 21 May 2022 20:29:20 +0200
Subject: [PATCH] fix: forward lean options to workers

---
 src/util/shell.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index 781d7d83fe..be80baf9d2 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -542,6 +542,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
                 try {
                     check_optarg("D");
                     opts = set_config_option(opts, optarg);
+                    forwarded_args.push_back(string_ref("-D" + std::string(optarg)));
                 } catch (lean::exception & ex) {
                     std::cerr << ex.what() << std::endl;
                     return 1;