git.annexia.org
/
goaljobs.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Implement // and quote.
[goaljobs.git]
/
goaljobs.mli
diff --git
a/goaljobs.mli
b/goaljobs.mli
index
07d717b
..
072fcef
100644
(file)
--- a/
goaljobs.mli
+++ b/
goaljobs.mli
@@
-171,6
+171,11
@@
val url_contains_string : string -> string -> bool
There is also a goal version of this function. *)
+val (//) : string -> string -> string
+ (** Concatenate two paths. *)
+
+val quote : string -> string
+ (** Quote the string to make it safe to pass directly to the shell. *)
(** {2 Shell}