inServer=true?

Author: datokrat

tests/lean/test_single.sh

@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
 diff_produced