diff options
| author | Hugo Herbelin | 2020-10-05 22:12:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-08 23:46:29 +0200 |
| commit | e18ed350f7b5710c382ea1306e7b1e7e2fb0c9f8 (patch) | |
| tree | e6da8700fc9cda554444510752aa1fa9123af4e4 /engine/termops.ml | |
| parent | 022632c074205bbe9fa3f992782e948c12cb7384 (diff) | |
Add a check of empty list of arguments in xmlprotocol where relevant.
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions