diff options
| author | Carst Tankink | 2014-10-09 15:39:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-13 18:13:21 +0200 |
| commit | 0253fc47be156d0d87cccda32c5bb90bc37960da (patch) | |
| tree | f5eac948b0a6eddceef5403185e5fb9760b8e628 /lib/feedback.mli | |
| parent | e1ea8a70094dfed28223d02dfca5d768737d4421 (diff) | |
When loading libraries, feed back dependencies.
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 775f71e9e5..d6d77b7cc4 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -44,6 +44,7 @@ type feedback_content = | ProcessingInMaster | Goals of Loc.t * string | StructuredGoals of Loc.t * xml + | FileDependency of string option * string | FileLoaded of string * string | Message of message |