diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/xmlprotocol.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index f1382fbcf..a4f133810 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -811,7 +811,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let n, s = to_pair to_string to_string ns in WorkerStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - (* | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) *) + | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -848,8 +848,8 @@ let of_feedback_content = function [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] - (* | Custom (loc, name, x) -> *) - (* constructor "feedback_content" "custom" [of_loc loc; of_string name; x] *) + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; |