Rename ServerEnv.env.edited_files -> editor_open_files
commitb9fbabc988a159fb385688f17c0eb369534f0071
authorWaleed Khan <waleedk@fb.com>
Fri, 17 Mar 2017 18:16:34 +0000 (17 11:16 -0700)
committerHhvm Bot <hhvm-bot@users.noreply.github.com>
Fri, 17 Mar 2017 18:21:52 +0000 (17 11:21 -0700)
treead85fc99aa2ac2969cb33d5bec2a79e6ff7ee0b8
parentf388f180d484f9ee9a19a1c6a40b34b9e2e2a367
Rename ServerEnv.env.edited_files -> editor_open_files

Summary: These files aren't actually the files being edited — they're just the files that are open in the editor, and thus might be edited in the future.

Reviewed By: michaeltingley

Differential Revision: D4725973

fbshipit-source-id: 7992539cbdbcaa624bae95dff7bd7801031ffa38
hphp/hack/src/server/serverEnv.ml
hphp/hack/src/server/serverEnvBuild.ml
hphp/hack/src/server/serverFileSync.ml
hphp/hack/src/server/serverMain.ml
hphp/hack/src/server/serverTypeCheck.ml