diff options
| author | Daniel Harding <33dannye@gmail.com> | 2019-01-13 22:36:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-13 22:36:13 -0600 |
| commit | 108245cb21abb3abac051b7db84ed6c694192a61 (patch) | |
| tree | b2638bbf850cdc2dca4cdb6d6db994b4735ca2bd /extras | |
| parent | 90430e6dee9e207dc0b618d07566f83617343f60 (diff) | |
| parent | 703224335280bf1170982113ac3d09fe198c0564 (diff) | |
Merge pull request #195 from Rangi42/master
Remove 'extras' submodule; and add 'make tidy'
Diffstat (limited to 'extras')
| m--------- | extras | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/extras b/extras deleted file mode 160000 -Subproject be6d6c9ce9a86231482eafacd4be86728580936 |