diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 16:40:30 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 16:43:15 +0200 |
| commit | cc6957b0dbb19a4c0ca505650d252d9486088a5f (patch) | |
| tree | 4a3d2bce53ea2bd8450fd0c2813e074e21d02c63 /parsing/cLexer.ml4 | |
| parent | 0d5abcf9e17b4fe0462ffa60d04a321d2707ccf6 (diff) | |
Fix #4941 - ~/.coqrc file confusing locations
Diffstat (limited to 'parsing/cLexer.ml4')
| -rw-r--r-- | parsing/cLexer.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 2acccfdf5..bec891f7f 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -103,6 +103,9 @@ open Error let current_file = ref "" +let get_current_file () = + !current_file + let set_current_file ~fname = current_file := fname |