aboutsummaryrefslogtreecommitdiffstats
path: root/tools
diff options
context:
space:
mode:
authorBernhard Schommer <bernhard@bernhard-ThinkPad-W520.(none)>2015-02-26 23:52:05 +0100
committerBernhard Schommer <bernhard@bernhard-ThinkPad-W520.(none)>2015-02-26 23:52:05 +0100
commitfd204b20e4ac3c41e1826f99344023d294a834c0 (patch)
tree0968dafa0e53bae65254b44d6e560060f779ef19 /tools
parent6d53a8b7ffd06d9726103803eb69d94a333ae0a5 (diff)
downloadcompcert-kvx-fd204b20e4ac3c41e1826f99344023d294a834c0.tar.gz
compcert-kvx-fd204b20e4ac3c41e1826f99344023d294a834c0.zip
Removed the glob files from doc/ instead of doc/glob/
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions