| commit | d07488429b3003f220dba8ad4240ed8a2b743474 | [log] [tgz] |
|---|---|---|
| author | Paul Wankadia <junyer@google.com> | Mon Feb 13 10:04:02 2023 -0800 |
| committer | Paul Wankadia <junyer@google.com> | Mon Feb 13 18:05:49 2023 +0000 |
| tree | 18ca47eef1ef2045c8135e87f383d4ad23089b20 | |
| parent | 891fa668468f201f6a0c16bbff76f26d8ae59e82 [diff] |
Use `PUBLIC_HEADER` to install headers. Change-Id: I8d7a1b51deb35773d95af2ec1b7a866c8700f0d7 Reviewed-on: https://code-review.googlesource.com/c/re2/+/61030 Reviewed-by: Alex Chernyakhovsky <achernya@google.com> Reviewed-by: Paul Wankadia <junyer@google.com>