Skip to content

Commit

Permalink
Apply CR comments
Browse files Browse the repository at this point in the history
  • Loading branch information
marianaalanis93 committed May 20, 2022
1 parent 4956ef5 commit 255d42d
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 4 deletions.
1 change: 1 addition & 0 deletions lean4-infoview/src/infoview/info.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
</div>
{nothingToShow && (
isPaused ?
/* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
<span>Updating is paused.{' '}
<a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerDisplayUpdate(); }}>Refresh</a>
{' '}or <a className="link pointer dim" onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
Expand Down
9 changes: 5 additions & 4 deletions vscode-lean4/src/utils/fsHelper.ts
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,11 @@ export async function fileExists(pathFile: PathLike): Promise<boolean> {
}

/**
* fill this in later
* @param file
* @param folder
* @returns
* This helper function is used to check if an specific file is in certain Folder.
* it also checks some cases with Windows (windows paths are case insensitive.)
* @param file string that contains a file name that will be checked if it exists in a certain folder.
* @param folder string that contains a folder name where it will check if a certain file exists
* @returns a boolean that says if the file exists in folder
*/
export function isFileInFolder(file: string, folder: string){
if (process.platform === 'win32') {
Expand Down
1 change: 1 addition & 0 deletions vscode-lean4/test/suite/utils/helpers.ts
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,7 @@ export async function restartLeanServer(client: LeanClient, retries=30, delay=10

// check we have no errors.
const actual = stateChanges.toString();
console.log('actua'+actual)

This comment has been minimized.

Copy link
@lovettchris

lovettchris May 20, 2022

Contributor

typo "actua"

assert(actual === 'stopped,restarted');
return false;
}
Expand Down

0 comments on commit 255d42d

Please sign in to comment.