aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-08-30 16:40:30 +0200
committerMaxime Dénès2016-08-30 16:43:15 +0200
commitcc6957b0dbb19a4c0ca505650d252d9486088a5f (patch)
tree4a3d2bce53ea2bd8450fd0c2813e074e21d02c63 /kernel/nativecode.ml
parent0d5abcf9e17b4fe0462ffa60d04a321d2707ccf6 (diff)
Fix #4941 - ~/.coqrc file confusing locations
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions