aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorEnrico Tassi2017-08-29 13:54:46 +0200
committerEnrico Tassi2017-08-29 17:47:57 +0200
commita93279fb7fe5917ab859e7b3dfb6f89522161419 (patch)
treeaeec78aa7cf69075e631fcd247fd4141d81beddc /plugins/syntax/string_syntax.ml
parent6e07e3a53e56882043b9db49f03fdf1470a16c46 (diff)
coq_makefile: print error message when coqlib is not set properly
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions