diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 01:50:26 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:10 -0400 |
| commit | 92b61209c60b368bbc095950786187b94b167632 (patch) | |
| tree | 5cceb7b23780618d89143d674aca2b3ccb481742 /dev/ci | |
| parent | 139d206294f98194e9bdb19a7d5da73f9b104db5 (diff) | |
[declare] Remove one use of inline_private_constants
We instead favor the `build_by_tactic` function which should at some
point better integrated in the declare core.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions