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 | |
| 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')
0 files changed, 0 insertions, 0 deletions