aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/objects.el
diff options
context:
space:
mode:
authorArnaud Spiwack2014-10-17 16:23:01 +0200
committerArnaud Spiwack2014-10-22 07:31:45 +0200
commitaa64260119704620540017a23815cd7c40c3cff3 (patch)
tree677157e51849510130e868d93193fa8c4b3f1ca2 /dev/tools/objects.el
parenta5a355ec3e9cbbfa28be53b9ba6ef914136b0aba (diff)
Proofview: remove a redundant primitive.
Diffstat (limited to 'dev/tools/objects.el')
0 files changed, 0 insertions, 0 deletions