diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 02:59:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-19 02:59:42 +0200 |
| commit | a2b23ba26066944685e6c5a58e8cfc87c3aa9a2c (patch) | |
| tree | ef07207d4b5aa870cf6a9ed4e833e7fda6d57af0 /dev | |
| parent | 306f862507c278f6865b82e5443f9d47742b2bc5 (diff) | |
[pcoq] Remove unneeded casting operators.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions