projects
/
tatoo.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(from parent 1:
24436e9
)
Add a bullet symbol.
author
Kim Nguyễn
<kn@lri.fr>
Wed, 17 Jul 2013 16:00:58 +0000
(18:00 +0200)
committer
Kim Nguyễn
<kn@lri.fr>
Wed, 17 Jul 2013 16:10:01 +0000
(18:10 +0200)
src/pretty.ml
patch
|
blob
|
history
src/pretty.mli
patch
|
blob
|
history
diff --git
a/src/pretty.ml
b/src/pretty.ml
index
e64edab
..
6d1dd46
100644
(file)
--- a/
src/pretty.ml
+++ b/
src/pretty.ml
@@
-86,6
+86,7
@@
let up_arrow = "↑"
let right_arrow = "→"
let left_arrow = "←"
let epsilon = "ϵ"
+let bullet = "•"
let big_sigma = "∑"
let cap = "∩"
let cup = "∪"
diff --git
a/src/pretty.mli
b/src/pretty.mli
index
ee828d5
..
96fb773
100644
(file)
--- a/
src/pretty.mli
+++ b/
src/pretty.mli
@@
-22,6
+22,7
@@
val up_arrow : string
val right_arrow : string
val left_arrow : string
val epsilon : string
+val bullet : string
val big_sigma : string
val cap : string
val cup : string