diff --git a/collects/planet2/scribblings/planet2.scrbl b/collects/planet2/scribblings/planet2.scrbl index 2512bf0315..cc69db236a 100644 --- a/collects/planet2/scribblings/planet2.scrbl +++ b/collects/planet2/scribblings/planet2.scrbl @@ -153,14 +153,15 @@ is the directory name.} URLs is: @inset{@exec{github://github.com/}@nonterm{user}@exec{/}@nonterm{repository}@; -@exec{/}@nonterm{branch}@exec{/}@nonterm{optional-subpath}} +@exec{/}@nonterm{branch-or-tag}@exec{/}@nonterm{optional-subpath}} For example, @filepath{github://github.com/game/tic-tac-toe/master/} is a GitHub package source. -The @exec{zip}-formatted archive for the repository (generated by GitHub for -every branch) is used as a remote URL archive path, except the -@tech{checksum} is the hash identifying the branch. +The @exec{zip}-formatted archive for the repository (generated by +GitHub for every branch and tag) is used as a remote URL archive path, +except the @tech{checksum} is the hash identifying the branch (or +tag). A package source is inferred to be a GitHub reference when it starts with @litchar{github://}; a package source that is otherwise