aboutsummaryrefslogtreecommitdiff
path: root/lib/grep.ml
diff options
context:
space:
mode:
authorMarc Coquand <marc@mccd.space>2024-05-18 13:36:55 -0500
committerMarc Coquand <marc@mccd.space>2024-05-18 13:36:55 -0500
commitacb42d7250f4832e2c93e5ecfaab4dd69b4c4a11 (patch)
tree40d1123e90d13dfbedd20bc329dd85afe808aa1d /lib/grep.ml
parentf805a04bd0600653f71e5e4e006104892cf7b6b9 (diff)
downloadstitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.tar.gz
stitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.tar.bz2
stitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.zip
Arbitrary command for article
Diffstat (limited to '')
-rw-r--r--lib/grep.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/grep.ml b/lib/grep.ml
index 5690edc..c5acbb6 100644
--- a/lib/grep.ml
+++ b/lib/grep.ml
@@ -292,6 +292,11 @@ type display_type =
| Bold of string
| Normal of string
+let display_type_line = function
+ | Bold s -> s
+ | Normal s -> s
+
+
let pretty_print_parsed_content parsed_files =
let padding = String.make headline_pattern_length ' ' in
List.concat_map