diff options
| author | Emilio Jesus Gallego Arias | 2020-04-30 16:44:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-30 16:44:37 +0200 |
| commit | ebf2619804184065604f801891850e8de3c146be (patch) | |
| tree | 3a9b1cc8395c97714a407ab30872099124647254 /dev/ci | |
| parent | d436c45a19de2f91aad94f492b547225f8c5b305 (diff) | |
| parent | 3034677ef9103262f8ed2e632bec843d25f9b25f (diff) | |
Merge PR #12216: Remove outdated code and comments in Declare.
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions