From 6a9997c7ad8d401eedc1dba53ce5b9fc9d67d0cf Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 25 Sep 2021 23:59:13 -0400
Subject: [PATCH] chore: `-O3` not `-03`

---
 Lake/Package.lean | 2 +-
 README.md         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lake/Package.lean b/Lake/Package.lean
index 6d6c2e8388..a3d0dba209 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -172,7 +172,7 @@ structure PackageConfig where
   /--
     Additional arguments to pass to `leanc`
     while compiling the C source files generated by `lean`.
-    Defaults to `-03` and `-DNDEBUG`.
+    Defaults to `-O3` and `-DNDEBUG`.
   -/
   leancArgs : Array String := #["-O3", "-DNDEBUG"]
 
diff --git a/README.md b/README.md
index 646b47c6b7..25ec0d32af 100644
--- a/README.md
+++ b/README.md
@@ -82,7 +82,7 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Library / Binary Compilation
 
-* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Defaults to `-03` and `-DNDEBUG`.
+* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Defaults to `-O3` and `-DNDEBUG`.
 * `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`.
 * `libName`: The name of the package's static library. Defaults to the string representation of the package's `moduleRoot`.
 * `libDir`: The build subdirectory to which Lake should output the package's static library. Defaults to `lib`.