File tree Expand file tree Collapse file tree 3 files changed +5
-3
lines changed
Expand file tree Collapse file tree 3 files changed +5
-3
lines changed Original file line number Diff line number Diff line change 1212
1313source " $( realpath " $( dirname " $0 " ) " ) /transcript_helpers.sh"
1414
15+ echo " UCM Version: $( transcript_ucm --version) "
16+
1517# Base directory containing share-api transcripts
1618transcripts_location=" transcripts/share-apis"
1719
Original file line number Diff line number Diff line change @@ -45,7 +45,7 @@ Push and pull it back.
4545``` ucm
4646proj/main> push @transcripts/proj/main
4747
48- Uploaded 464 entities.
48+ Uploaded 466 entities.
4949
5050 I just created @transcripts/proj on http://localhost:5424
5151
@@ -71,7 +71,7 @@ proj/pulled> ls .
7171 4. B. (2 terms)
7272 5. a ('Nat)
7373 6. b ('Nat)
74- 7. builtin. (667 terms, 104 types)
74+ 7. builtin. (676 terms, 107 types)
7575 8. xs (['Nat])
7676 9. ys ([Nat])
7777```
Original file line number Diff line number Diff line change @@ -11,7 +11,7 @@ mkdir -p "${ucm_xdg_data_dir}/unisonlanguage"
1111ucm_credentials_file=" ${ucm_xdg_data_dir} /unisonlanguage/credentials.json"
1212
1313# Executable to use when running unison transcripts
14- export UCM_PATH=" ${1 :- " $( which ucm) " } "
14+ export UCM_PATH=" ${UCM_PATH :- " $( which ucm) " } "
1515export empty_causal_hash=' sg60bvjo91fsoo7pkh9gejbn0qgc95vra87ap6l5d35ri0lkaudl7bs12d71sf3fh6p23teemuor7mk1i9n567m50ibakcghjec5ajg'
1616export echo_server_port=9999
1717export echo_server=" http://localhost:${echo_server_port} "
You can’t perform that action at this time.
0 commit comments