diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index b7afc0e118..a7e65d319f 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -41,7 +41,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
   let p   := andthenFn whitespace Module.header.fn
   let tokens := Module.updateTokens (getTokenTable dummyEnv)
   let s   := p.run inputCtx { env := dummyEnv, options := {} } tokens (mkParserState inputCtx.input)
-  let stx := s.stxStack.back
+  let stx := if s.stxStack.isEmpty then .missing else s.stxStack.back
   match s.errorMsg with
   | some errorMsg =>
     let msg := mkErrorMessage inputCtx s.pos (toString errorMsg)
diff --git a/tests/lean/2006.lean b/tests/lean/2006.lean
new file mode 100644
index 0000000000..84340a0b61
--- /dev/null
+++ b/tests/lean/2006.lean
@@ -0,0 +1 @@
+/-
diff --git a/tests/lean/2006.lean.expected.out b/tests/lean/2006.lean.expected.out
new file mode 100644
index 0000000000..bcf16e23af
--- /dev/null
+++ b/tests/lean/2006.lean.expected.out
@@ -0,0 +1 @@
+2006.lean:2:0: error: unterminated comment