summaryrefslogtreecommitdiff
path: root/Ch10.idr
diff options
context:
space:
mode:
authorKjetil Orbekk <kjetil.orbekk@gmail.com>2017-02-16 08:18:44 -0500
committerKjetil Orbekk <kjetil.orbekk@gmail.com>2017-02-16 08:18:44 -0500
commit03f09725cb5f162ae19eba5bba188f085a0c11a7 (patch)
treefb91917a4ede0ce3178c4b7fb6884e10886cfa99 /Ch10.idr
parent65757403924d51f6cc32a30ad7282996ace61854 (diff)
Use an interface for dispatching.HEADmaster
Diffstat (limited to 'Ch10.idr')
0 files changed, 0 insertions, 0 deletions