diff options
| author | Théo Zimmermann | 2020-03-18 17:11:03 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-18 17:11:03 +0100 |
| commit | 55490662517966d01a53ddd708709d1fc739286c (patch) | |
| tree | 368e941af3ca3d63de2921bb59ace8ac88e6e5a8 /plugins | |
| parent | 4c2a4890b75d516acfeccdb4105e46760239a7f1 (diff) | |
| parent | c685a8a3690b3345dbc2770530e3da1b6639a654 (diff) | |
Merge PR #11812: Add an Export locality to hints
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 82c64a9857..c43018022e 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -249,7 +249,8 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality locality) + let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality (match dbnames with None -> ["core"] | Some l -> l) entry; } END |