diff options
| author | Marc Coquand <marc@mccd.space> | 2024-05-18 13:36:55 -0500 |
|---|---|---|
| committer | Marc Coquand <marc@mccd.space> | 2024-05-18 13:36:55 -0500 |
| commit | acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11 (patch) | |
| tree | 40d1123e90d13dfbedd20bc329dd85afe808aa1d /lib/grep.ml | |
| parent | f805a04bd0600653f71e5e4e006104892cf7b6b9 (diff) | |
| download | stitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.tar.gz stitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.tar.bz2 stitch-acb42d7250f4832e2c93e5ecfaab4dd69b4c4a11.zip | |
Arbitrary command for article
Diffstat (limited to 'lib/grep.ml')
| -rw-r--r-- | lib/grep.ml | 5 |
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 |