only read counters when profile_log option is set
commit3ea69369deed9f8e2c44bbdc72cb2a4d8a7bf0c3
authorCatherine Gasnier <catg@fb.com>
Wed, 30 Sep 2020 15:16:20 +0000 (30 08:16 -0700)
committerFacebook GitHub Bot <facebook-github-bot@users.noreply.github.com>
Wed, 30 Sep 2020 15:18:28 +0000 (30 08:18 -0700)
tree8dd1c6c990fd32314f687426f05c3835b94a08df
parent18d305bc4cc285d45d567409113ab3460bf112ad
only read counters when profile_log option is set

Summary: ... to avoid possibly expensive system calls

Differential Revision: D21740519

fbshipit-source-id: 0810f46acd834ef1fc1287bd33f39e8d90f47a03
hphp/hack/src/typing/typing_check_service.ml