diff options
author | Lukacs Berki <lberki@google.com> | 2016-06-28 15:25:44 +0000 |
---|---|---|
committer | Dmitry Lomov <dslomov@google.com> | 2016-06-29 08:53:33 +0000 |
commit | 3cd00496502a335a958490be3308f39796d114ba (patch) | |
tree | 89f4dedf461e9a0307a9770bd7d637425c0346a0 /src/main/java/com/google/devtools/build/lib/flags | |
parent | cf738441e9cdda0f9d08861cb316596f77821baa (diff) |
Do not be satisfied with a JRE when looking for JNI headers.
--
MOS_MIGRATED_REVID=126076585
Diffstat (limited to 'src/main/java/com/google/devtools/build/lib/flags')
0 files changed, 0 insertions, 0 deletions