diff --git a/bin/leanc.in b/bin/leanc.in
index 90cef28bba..9bed536465 100644
--- a/bin/leanc.in
+++ b/bin/leanc.in
@@ -11,26 +11,36 @@
 set -e
 bindir=$(dirname $0)
 
-# Check C compiler
-for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
-    if [ -f $cc ] || command -v $cc; then
-        export LEAN_CC=$cc && break
-    fi
+# As an optimization, we use a C compiler for compiling object files without linking.
+# C files produced by Lean are also valid C++ files, but C compilers tend to be faster.
+# Final linking still has to be done by a C++ compiler because we need to link against the
+# Lean runtime written in C++ (https://isocpp.org/wiki/faq/mixing-c-and-cpp#overview-mixing-langs).
+use_c=maybe
+for arg in "$@"; do
+    [[ $use_c == maybe && $arg == "-c" ]] && use_c=yes
+    [[ $arg == "*.cpp" ]] && use_c=no
 done
-[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
 
-# Check C++ compiler
-for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
-    if [ -f $cxx ] || command -v $cxx; then
-        export LEAN_CXX=$cxx && break
-    fi
-done
-[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
+if [[ $use_c == yes ]]; then
+    # Check C compiler
+    for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
+        if [ -f $cc ] || command -v $cc; then
+            export LEAN_CC=$cc && break
+        fi
+    done
+    [ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
+
+    # NOTE: leanstatic and leanstdlib are cyclically dependent
+    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+else
+    # Check C++ compiler
+    for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
+        if [ -f $cxx ] || command -v $cxx; then
+            export LEAN_CXX=$cxx && break
+        fi
+    done
+    [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
 
-# Use C++ compiler if input contains substring ".cpp"
-if [[ "$@" == *".cpp"* ]]; then
     # NOTE: leanstatic and leanstdlib are cyclically dependent
     $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
-else
-    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
 fi