diff --git a/Makefile b/Makefile
index d6b26d9ee40..9be23b6b9ae 100644
--- a/Makefile
+++ b/Makefile
@@ -15,8 +15,13 @@ all-packages: package-1 package-2 package-src-1 package-src-2
 
 ### STAGES
 
+# For developers: you can set this variable externally, pointing
+# to a local build of stage0, to avoid recompiling it every time.
 ifneq ($(FSTAR_EXTERNAL_STAGE0),)
 FSTAR0_EXE := $(abspath $(FSTAR_EXTERNAL_STAGE0))
+_ != mkdir -p stage0/bin
+_ != ln -Trsf $(FSTAR0_EXE) stage0/bin/fstar.exe
+# ^ Setting this link allows VS code to work seamlessly.
 endif
 
 # When stage0 is bumped, use this:
diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk
index 260a3467d7e..3a0c740ef56 100644
--- a/mk/src_package_mk.mk
+++ b/mk/src_package_mk.mk
@@ -72,8 +72,8 @@ check_fstarc: install_bin
 	  SRC=src/ \
 	  FSTAR_EXE=$(call cygpath,out/bin/fstar.exe) \
 	  CACHE_DIR=fstarc.checked/ \
-	  CODEGEN=None \
-	  OUTPUT_DIR=None \
+	  CODEGEN=none \
+	  OUTPUT_DIR=none \
 	  TAG=fstarc \
 	  FSTAR_LIB=$(call cygpath,ulib) \
 	  FSTAR_ROOT=$(CURDIR) \