diff --git a/doc/examples/compiler/README.md b/doc/examples/compiler/README.md
index b2f7ea8b76..59a10315e2 100644
--- a/doc/examples/compiler/README.md
+++ b/doc/examples/compiler/README.md
@@ -1,9 +1,6 @@
 In this example, we use the Lean C code generator to construct a simple program.
 
-1- Generate `build/bin/test` program using `leanmake` (assuming `bin/` from e.g. the stage 0.5 build directory is in your `PATH`)
-```
-leanmake bin PKG=test
-```
+1- Generate `build/bin/test` program using `leanmake bin` (assuming `bin/` from e.g. the stage 0.5 build directory is in your `PATH`)
 
 2- Execute test program
 ```
diff --git a/src/bin/leanmake b/src/bin/leanmake
index 0d527c65b4..7a04a26417 100755
--- a/src/bin/leanmake
+++ b/src/bin/leanmake
@@ -7,6 +7,7 @@
 # * `leanmake PKG=Foo`  # compile package Foo into .olean files (in `build/Foo`, by default)
 # * `leanmake bin PKG=Foo`  # build the binary `build/bin/Foo`
 # * `leanmake lib PKG=Foo`  # build the library `build/lib/libFoo.a`
+# If there is exactly one .lean file in the current directory, you can omit `PKG`
 
 set -euo pipefail
 
diff --git a/src/lean.mk.in b/src/lean.mk.in
index 7a387e6db3..a27f1dedeb 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -1,6 +1,15 @@
 # Copyright (c) 2018 Simon Hudon. All rights reserved.
 # Released under Apache 2.0 license as described in the file LICENSE.
 # Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
+
+# We compile all source files in $PKG/ as well as $PKG.lean. $PKG is also used for naming binary files.
+ifndef PKG
+  PKG = $(strip $(subst .lean,, $(wildcard *.lean)))
+  ifneq ($(words $(PKG)), 1)
+    $(error no unique .lean file found in current directory, please specify PKG)
+  endif
+endif
+
 OUT = build
 OLEAN_OUT = $(OUT)
 TEMP_OUT = $(OUT)/temp
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index c1f933baac..2ca9e70ce7 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -88,7 +88,7 @@ add_test(NAME leancomptest_foreign
          COMMAND bash -c "${LEAN_BIN}/leanmake && ./build/bin/test")
 add_test(NAME leancomptest_doc_example
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
-         COMMAND bash -c "${LEAN_BIN}/leanmake bin PKG=test && ./build/bin/test hello world")
+         COMMAND bash -c "${LEAN_BIN}/leanmake bin && ./build/bin/test hello world")
 
 # LEAN INTERPRETER TESTS
 file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")