diff options
Diffstat (limited to 'generator/generator_utils.ml')
| -rw-r--r-- | generator/generator_utils.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/generator/generator_utils.ml b/generator/generator_utils.ml index 2bdcc0d8..b7401db0 100644 --- a/generator/generator_utils.ml +++ b/generator/generator_utils.ml @@ -303,3 +303,5 @@ let pod2text ~width name longdesc = pod2text_memo_updated (); lines +(* Compare two actions (for sorting). *) +let action_compare (n1,_,_,_,_,_,_) (n2,_,_,_,_,_,_) = compare n1 n2 |